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]

let k be Nat; :: thesis:
assume A4: S₁[k] ; :: thesis:
let X be finite set ; :: thesis:
assume that
A5: card X = k + 1 and
A6: X is Subset of F₁() ; :: thesis:
given x being Element of F₁() such that A7: x in X and
A8: P₁[x] ; :: thesis:
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;

suppose ex z being Element of F₁() st
( z in Xmx & P₁[z] ) ; :: thesis:

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 ;

suppose A14: not x <~ z ; :: thesis:

take z ; :: thesis:
thus z in X by A11; :: thesis:
thus P₁[z] by A12; :: thesis:

hereby :: thesis:

let y be Element of F₁(); :: thesis:
assume that
A15: y in X and
A16: y <~ z ; :: thesis:

per cases by A10, A15, XBOOLE_0:def 3;

suppose y in Xmx ; :: thesis:

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

end;

suppose y in {x} ; :: thesis:

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

end;

suppose A17: x <~ z ; :: thesis:

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 ;

suppose A24: v = x ; :: thesis:

take v ; :: thesis:
thus v in X by A21; :: thesis:
thus P₁[v] by A22; :: thesis:

hereby :: thesis:

let y be Element of F₁(); :: thesis:
assume that
A25: y in X and
A26: y <~ v ; :: thesis:

per cases by A18, A25, XBOOLE_0:def 3;

suppose y in Xmz ; :: thesis:

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

end;

suppose y in {z} ; :: thesis:

then z <~ x by A24, A26, TARSKI:def 1;
hence P₁[y] by A17; :: thesis:

end;

suppose A27: v <> x ; :: thesis:

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

per cases by A27, A28, Th27;

suppose A29: v <~ x ; :: thesis:

take v ; :: thesis:
thus v in X by A21; :: thesis:
thus P₁[v] by A22; :: thesis:

hereby :: thesis:

let y be Element of F₁(); :: thesis:
assume that
A30: y in X and
A31: y <~ v ; :: thesis:

per cases by A18, A30, XBOOLE_0:def 3;

suppose y in Xmz ; :: thesis:

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

end;

suppose y in {z} ; :: thesis:

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

end;

suppose A32: v =~ x ; :: thesis:

take x ; :: thesis:
thus x in X by A7; :: thesis:
thus P₁[x] by A8; :: thesis:

hereby :: thesis:

let y be Element of F₁(); :: thesis:
assume that
A33: y in X and
A34: y <~ x ; :: thesis:

per cases by A18, A33, XBOOLE_0:def 3;

suppose A35: y in Xmz ; :: thesis:

y <~ v

proof

assume A36: not y <~ v ; :: thesis:

per cases ;

suppose v = y ; :: thesis:

hence contradiction by A34, A32; :: thesis:

end;

suppose v <> y ; :: thesis:

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

end;

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

end;

suppose y in {z} ; :: thesis:

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

end;

suppose A37: for z being Element of F₁() st z in Xmx holds
not P₁[z] ; :: thesis:

take x ; :: thesis:
thus x in X by A7; :: thesis:
thus P₁[x] by A8; :: thesis:

hereby :: thesis:

let y be Element of F₁(); :: thesis:
assume that
A38: y in X and
A39: y <~ x ; :: thesis:

per cases by A10, A38, XBOOLE_0:def 3;

suppose y in Xmx ; :: thesis:

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

end;

suppose y in {x} ; :: thesis:

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

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₂() & y <~ x holds
not P₁[y] ) ) by A1; :: thesis: