defpred S₁[ Nat] means for X being finite set st card X = $1 & X is Subset of F₁() & ex x being Element of F₁() st
( x in X & P₁[x] ) holds
ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) );
A2: S₁[ 0 ] ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
let X be finite set ; :: thesis: ( card X = k + 1 & X is Subset of F₁() & ex x being Element of F₁() st
( x in X & P₁[x] ) implies ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) ) )
assume that
A5: card X = k + 1 and
A6: X is Subset of F₁() ; :: thesis: ( for x being Element of F₁() holds
( not x in X or not P₁[x] ) or ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) ) )
given x being Element of F₁() such that A7: x in X and
A8: P₁[x] ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )
set Xmx = X \ {x};
reconsider Xmx = X \ {x} as Subset of F₁() by A6, XBOOLE_1:1;
A9: card Xmx = (card X) - (card {x}) by A7, ZFMISC_1:31, CARD_2:44
.= (card X) - 1 by CARD_1:30
.= k by A5 ;
A10: Xmx \/ {x} = X by A7, ZFMISC_1:116;

per cases ( ex z being Element of F₁() st
( z in Xmx & P₁[z] ) or for z being Element of F₁() st z in Xmx holds
not P₁[z] ) ;

suppose ex z being Element of F₁() st
( z in Xmx & P₁[z] ) ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

then consider z being Element of F₁() such that
A11: z in Xmx and
A12: P₁[z] and
A13: for y being Element of F₁() st y in Xmx & y >~ z holds
not P₁[y] by A4, A9;

per cases ( not x >~ z or x >~ z ) ;

suppose A14: not x >~ z ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

take z ; :: thesis: ( z in X & P₁[z] & ( for y being Element of F₁() st y in X & y >~ z holds
not P₁[y] ) )
thus z in X by A11; :: thesis: ( P₁[z] & ( for y being Element of F₁() st y in X & y >~ z holds
not P₁[y] ) )
thus P₁[z] by A12; :: thesis: for y being Element of F₁() st y in X & y >~ z holds
not P₁[y]

hereby :: thesis: verum

let y be Element of F₁(); :: thesis: ( y in X & y >~ z implies not P₁[b₁] )
assume that
A15: y in X and
A16: y >~ z ; :: thesis: P₁[b₁]

per cases ( y in Xmx or y in {x} ) by A10, A15, XBOOLE_0:def 3;

suppose y in Xmx ; :: thesis: P₁[b₁]

hence P₁[y] by A16, A13; :: thesis: verum

end;

suppose y in {x} ; :: thesis: P₁[b₁]

hence P₁[y] by A14, A16, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

suppose A17: x >~ z ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

set Xmz = X \ {z};
reconsider Xmz = X \ {z} as Subset of F₁() by A6, XBOOLE_1:1;
A18: Xmz \/ {z} = X by A11, ZFMISC_1:116;
A19: card Xmz = (card X) - (card {z}) by A11, ZFMISC_1:31, CARD_2:44
.= (card X) - 1 by CARD_1:30
.= k by A5 ;
A20: x in Xmz by A7, A17, ZFMISC_1:56;
then consider v being Element of F₁() such that
A21: v in Xmz and
A22: P₁[v] and
A23: for y being Element of F₁() st y in Xmz & y >~ v holds
not P₁[y] by A19, A4, A8;

per cases ( v = x or v <> x ) ;

suppose A24: v = x ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

take v ; :: thesis: ( v in X & P₁[v] & ( for y being Element of F₁() st y in X & y >~ v holds
not P₁[y] ) )
thus v in X by A21; :: thesis: ( P₁[v] & ( for y being Element of F₁() st y in X & y >~ v holds
not P₁[y] ) )
thus P₁[v] by A22; :: thesis: for y being Element of F₁() st y in X & y >~ v holds
not P₁[y]

hereby :: thesis: verum

let y be Element of F₁(); :: thesis: ( y in X & y >~ v implies not P₁[b₁] )
assume that
A25: y in X and
A26: y >~ v ; :: thesis: P₁[b₁]

per cases ( y in Xmz or y in {z} ) by A18, A25, XBOOLE_0:def 3;

suppose y in Xmz ; :: thesis: P₁[b₁]

hence P₁[y] by A26, A23; :: thesis: verum

end;

suppose y in {z} ; :: thesis: P₁[b₁]

hence P₁[y] by A17, A24, A26, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

suppose A27: v <> x ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

A28: not F₁() is empty by A6, A7;
not x >~ v by A20, A8, A23;

per cases then ( v >~ x or v =~ x ) by A27, A28, Th27;

suppose A29: v >~ x ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

take v ; :: thesis: ( v in X & P₁[v] & ( for y being Element of F₁() st y in X & y >~ v holds
not P₁[y] ) )
thus v in X by A21; :: thesis: ( P₁[v] & ( for y being Element of F₁() st y in X & y >~ v holds
not P₁[y] ) )
thus P₁[v] by A22; :: thesis: for y being Element of F₁() st y in X & y >~ v holds
not P₁[y]

hereby :: thesis: verum

let y be Element of F₁(); :: thesis: ( y in X & y >~ v implies not P₁[b₁] )
assume that
A30: y in X and
A31: y >~ v ; :: thesis: P₁[b₁]

per cases ( y in Xmz or y in {z} ) by A18, A30, XBOOLE_0:def 3;

suppose y in Xmz ; :: thesis: P₁[b₁]

hence P₁[y] by A31, A23; :: thesis: verum

end;

suppose y in {z} ; :: thesis: P₁[b₁]

then z >~ v by A31, TARSKI:def 1;
hence P₁[y] by A17, A29, ORDERS_2:3; :: thesis: verum

end;

end;

end;

end;

suppose A32: v =~ x ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

take x ; :: thesis: ( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )
thus x in X by A7; :: thesis: ( P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )
thus P₁[x] by A8; :: thesis: for y being Element of F₁() st y in X & y >~ x holds
not P₁[y]

hereby :: thesis: verum

let y be Element of F₁(); :: thesis: ( y in X & y >~ x implies not P₁[b₁] )
assume that
A33: y in X and
A34: y >~ x ; :: thesis: P₁[b₁]

per cases ( y in Xmz or y in {z} ) by A18, A33, XBOOLE_0:def 3;

suppose A35: y in Xmz ; :: thesis: P₁[b₁]

y >~ v

proof

assume A36: not y >~ v ; :: thesis: contradiction

per cases ( v = y or v <> y ) ;

suppose v = y ; :: thesis: contradiction

hence contradiction by A34, A32; :: thesis: verum

end;

suppose v <> y ; :: thesis: contradiction

then v >= y by A36, A28, Th27;
hence contradiction by A34, A32, ORDERS_2:3; :: thesis: verum

end;

end;

end;

hence P₁[y] by A35, A23; :: thesis: verum

end;

suppose y in {z} ; :: thesis: P₁[b₁]

then z >~ x by TARSKI:def 1, A34;
hence P₁[y] by A17; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

end;

suppose A37: for z being Element of F₁() st z in Xmx holds
not P₁[z] ; :: thesis: ex x being Element of F₁() st
( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )

take x ; :: thesis: ( x in X & P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )
thus x in X by A7; :: thesis: ( P₁[x] & ( for y being Element of F₁() st y in X & y >~ x holds
not P₁[y] ) )
thus P₁[x] by A8; :: thesis: for y being Element of F₁() st y in X & y >~ x holds
not P₁[y]

hereby :: thesis: verum

let y be Element of F₁(); :: thesis: ( y in X & y >~ x implies not P₁[b₁] )
assume that
A38: y in X and
A39: y >~ x ; :: thesis: P₁[b₁]

per cases ( y in Xmx or y in {x} ) by A10, A38, XBOOLE_0:def 3;

suppose y in Xmx ; :: thesis: P₁[b₁]

hence P₁[y] by A37; :: thesis: verum

end;

suppose y in {x} ; :: thesis: P₁[b₁]

hence P₁[y] by A39, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;

A40: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
reconsider c = card F₂() as Nat ;
S₁[c] by A40;
hence ex x being Element of F₁() st
( x in F₂() & P₁[x] & ( for y being Element of F₁() st y in F₂() & x <~ y holds
not P₁[y] ) ) by A1; :: thesis: verum