defpred S1[ Nat] means for A being Subset of F1() st $1 + 1 = card A holds
ex x being Element of F1() st
( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) );
A1: ((card F1()) -' 1) + 1 = ((card F1()) - 1) + 1 by Th19
.= card F1() ;
A2: F1() c= F1() ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for A being Subset of F1() st (k + 1) + 1 = card A holds
ex x being Element of F1() st
( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) )
let A be Subset of F1(); :: thesis: ( (k + 1) + 1 = card A implies ex x being Element of F1() st
( b2 in x & ( for y being Element of F1() st b3 in x holds
F2(y) <= F2(b3) ) ) )
assume A5: (k + 1) + 1 = card A ; :: thesis: ex x being Element of F1() st
( b2 in x & ( for y being Element of F1() st b3 in x holds
F2(y) <= F2(b3) ) )
then A6: A <> {} ;
consider x being Element of A, C being Subset of A such that
A7: A = C \/ {x} and
A8: card C = k + 1 by A5, Th23;
x in A by A6;
then reconsider x = x as Element of F1() ;
reconsider C = C as Subset of F1() by XBOOLE_1:1;
consider z being Element of F1() such that
A9: z in C and
A10: for y being Element of F1() st y in C holds
F2(z) <= F2(y) by A4, A8;
per cases ( F2(x) <= F2(z) or F2(x) > F2(z) ) ;
suppose A11: F2(x) <= F2(z) ; :: thesis: ex x being Element of F1() st
( b2 in x & ( for y being Element of F1() st b3 in x holds
F2(y) <= F2(b3) ) )
take x = x; :: thesis: ( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) )
thus x in A by A6; :: thesis: for y being Element of F1() st y in A holds
F2(x) <= F2(y)
hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in A implies F2(x) <= F2(b1) )
assume A12: y in A ; :: thesis: F2(x) <= F2(b1)
per cases ( y in C or y in {x} ) by A7, A12, XBOOLE_0:def 3;
suppose y in C ; :: thesis: F2(x) <= F2(b1)
then F2(z) <= F2(y) by A10;
hence F2(x) <= F2(y) by A11, XXREAL_0:2; :: thesis: verum
end;
suppose y in {x} ; :: thesis: F2(x) <= F2(b1)
hence F2(x) <= F2(y) by TARSKI:def 1; :: thesis: verum
end;
end;
end;
end;
suppose A13: F2(x) > F2(z) ; :: thesis: ex z being Element of F1() st
( b2 in z & ( for y being Element of F1() st b3 in z holds
F2(y) <= F2(b3) ) )
take z = z; :: thesis: ( z in A & ( for y being Element of F1() st y in A holds
F2(z) <= F2(y) ) )
thus z in A by A9; :: thesis: for y being Element of F1() st y in A holds
F2(z) <= F2(y)
hereby :: thesis: verum
let y be Element of F1(); :: thesis: ( y in A implies F2(z) <= F2(b1) )
assume A14: y in A ; :: thesis: F2(z) <= F2(b1)
per cases ( y in C or y in {x} ) by A7, A14, XBOOLE_0:def 3;
suppose y in C ; :: thesis: F2(z) <= F2(b1)
hence F2(z) <= F2(y) by A10; :: thesis: verum
end;
suppose y in {x} ; :: thesis: F2(z) <= F2(b1)
hence F2(z) <= F2(y) by A13, TARSKI:def 1; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A15: S1[ 0 ]
proof
let A be Subset of F1(); :: thesis: ( 0 + 1 = card A implies ex x being Element of F1() st
( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) ) )
assume 0 + 1 = card A ; :: thesis: ex x being Element of F1() st
( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) )
then consider x being Element of A such that
A16: A = {x} by Th24;
reconsider x = x as Element of F1() by A16, ZFMISC_1:31;
take x ; :: thesis: ( x in A & ( for y being Element of F1() st y in A holds
F2(x) <= F2(y) ) )
thus x in A by A16; :: thesis: for y being Element of F1() st y in A holds
F2(x) <= F2(y)
thus for y being Element of F1() st y in A holds
F2(x) <= F2(y) by A16, TARSKI:def 1; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A15, A3);
 then ( ((card F1()) -' 1) + 1 = card F1() implies ex x being Element of F1() st
( x in F1() & ( for y being Element of F1() st y in F1() holds
F2(x) <= F2(y) ) ) ) by A2;
then consider x being Element of F1() such that
x in F1() and
A17: for y being Element of F1() st y in F1() holds
F2(x) <= F2(y) by A1;
take x ; :: thesis: for y being Element of F1() holds F2(x) <= F2(y)
let y be Element of F1(); :: thesis: F2(x) <= F2(y)
thus F2(x) <= F2(y) by A17; :: thesis: verum