set b = the Element of F2();
set M = { { ff where ff is Element of F2() : P1[tt,ff] } where tt is Element of F1() : tt in F3() } ;
set f = the Function of F1(),F2();
assume A2: for ff being Function of F1(),F2() ex t being Element of F1() st
( t in F3() & P1[t,ff . t] ) ; :: thesis: contradiction
then consider t being Element of F1() such that
A3: t in F3() and
P1[t, the Function of F1(),F2() . t] ;
{ ff where ff is Element of F2() : P1[t,ff] } in { { ff where ff is Element of F2() : P1[tt,ff] } where tt is Element of F1() : tt in F3() } by A3;
then reconsider M = { { ff where ff is Element of F2() : P1[tt,ff] } where tt is Element of F1() : tt in F3() } as non empty set ;
now :: thesis: for X being set st X in M holds
X <> {}
let X be set ; :: thesis: ( X in M implies X <> {} )
assume X in M ; :: thesis: X <> {}
then consider t being Element of F1() such that
A4: X = { ff where ff is Element of F2() : P1[t,ff] } and
A5: t in F3() ;
consider ff being Element of F2() such that
A6: P1[t,ff] by A1, A5;
ff in X by A4, A6;
hence X <> {} ; :: thesis: verum
end;
then consider Choice being Function such that
dom Choice = M and
A7: for X being set st X in M holds
Choice . X in X by FUNCT_1:111;
defpred S1[ Element of F1(), set ] means ( ( \$1 in F3() implies \$2 = Choice . { ff where ff is Element of F2() : P1[\$1,ff] } ) & ( \$1 in F3() or \$2 = the Element of F2() ) );
A8: now :: thesis: for t being Element of F1() ex y being Element of F2() st S1[t,y]
let t be Element of F1(); :: thesis: ex y being Element of F2() st S1[t,y]
A9: now :: thesis: ( t in F3() implies Choice . { ff where ff is Element of F2() : P1[t,ff] } is Element of F2() )
set s = { ff where ff is Element of F2() : P1[t,ff] } ;
assume t in F3() ; :: thesis: Choice . { ff where ff is Element of F2() : P1[t,ff] } is Element of F2()
then { ff where ff is Element of F2() : P1[t,ff] } in M ;
then Choice . { ff where ff is Element of F2() : P1[t,ff] } in { ff where ff is Element of F2() : P1[t,ff] } by A7;
then ex ff being Element of F2() st
( Choice . { ff where ff is Element of F2() : P1[t,ff] } = ff & P1[t,ff] ) ;
hence Choice . { ff where ff is Element of F2() : P1[t,ff] } is Element of F2() ; :: thesis: verum
end;
( t in F3() implies t in F3() ) ;
hence ex y being Element of F2() st S1[t,y] by A9; :: thesis: verum
end;
consider f being Function of F1(),F2() such that
A10: for x being Element of F1() holds S1[x,f . x] from
now :: thesis: for t being Element of F1() st t in F3() holds
P1[t,f . t]
let t be Element of F1(); :: thesis: ( t in F3() implies P1[t,f . t] )
assume A11: t in F3() ; :: thesis: P1[t,f . t]
then A12: { ff where ff is Element of F2() : P1[t,ff] } in M ;
f . t = Choice . { ff where ff is Element of F2() : P1[t,ff] } by ;
then f . t in { ff where ff is Element of F2() : P1[t,ff] } by ;
then ex ff being Element of F2() st
( f . t = ff & P1[t,ff] ) ;
hence P1[t,f . t] ; :: thesis: verum
end;
hence contradiction by A2; :: thesis: verum