let M be non limit_cardinal Aleph; :: thesis:
set N = predecessor M;
set GT = (nextcard (predecessor M)) \ (predecessor M);
defpred S₁[ object , object ] means ex f being Function st
( $2 = f & f is one-to-one & dom f = predecessor M & rng f = $1 );
A1: for K1 being object st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
ex x being object st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S₁[K1,x] )

let K1 be object ; :: thesis:
assume A2: K1 in (nextcard (predecessor M)) \ (predecessor M) ; :: thesis:
reconsider K2 = K1 as Element of nextcard (predecessor M) by A2;
not K1 in predecessor M by A2, XBOOLE_0:def 5;
then card (predecessor M) c= card K2 by CARD_1:11, ORDINAL1:16;
then A3: predecessor M c= card K2 ;
card K2 in nextcard (predecessor M) by CARD_1:9;
then card K2 c= predecessor M by CARD_3:91;
then card K2 = predecessor M by A3
.= card (predecessor M) ;
then K2, predecessor M are_equipotent by CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = predecessor M and
A6: rng f = K1 by WELLORD2:def 4;
rng f c= nextcard (predecessor M) by A2, A6, ORDINAL1:def 2;
then f in Funcs ((predecessor M),(nextcard (predecessor M))) by A5, FUNCT_2:def 2;
hence ex x being object st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S₁[K1,x] ) by A4, A5, A6; :: thesis:

end;

consider h1 being Function such that
A7: dom h1 = (nextcard (predecessor M)) \ (predecessor M) and
rng h1 c= Funcs ((predecessor M),(nextcard (predecessor M))) and
A8: for K1 being object st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
S₁[K1,h1 . K1] from FUNCT_1:sch 6(A1);
for K1 being object st K1 in dom h1 holds
h1 . K1 is Function

proof

let K1 be object ; :: thesis:
assume K1 in dom h1 ; :: thesis:
then ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A7, A8;
hence h1 . K1 is Function ; :: thesis:

end;

then reconsider h = h1 as Function-yielding Function by FUNCOP_1:def 6;
( predecessor M in nextcard (predecessor M) & not predecessor M in predecessor M ) by CARD_1:18;
then reconsider GT1 = (nextcard (predecessor M)) \ (predecessor M) as non empty set by XBOOLE_0:def 5;
deffunc H₁( set , set ) -> set = (h . $2) . $1;
defpred S₂[ set , set , set ] means $3 = { K2 where K2 is Element of GT1 : H₁($1,K2) = $2 } ;
A9: for N1 being Element of predecessor M
for K1 being Element of M ex S1 being Subset of GT1 st S₂[N1,K1,S1]

proof

let N1 be Element of predecessor M; :: thesis:
let K1 be Element of M; :: thesis:
defpred S₃[ set ] means H₁(N1,$1) = K1;
take { K2 where K2 is Element of GT1 : H₁(N1,K2) = K1 } ; :: thesis:
{ K2 where K2 is Element of GT1 : S₃[K2] } is Subset of GT1 from DOMAIN_1:sch 7();
hence ( { K2 where K2 is Element of GT1 : H₁(N1,K2) = K1 } is Subset of GT1 & S₂[N1,K1, { K2 where K2 is Element of GT1 : H₁(N1,K2) = K1 } ] ) ; :: thesis:

end;

consider T1 being Function of [:(predecessor M),M:],(bool GT1) such that
A10: for N1 being Element of predecessor M
for K1 being Element of M holds S₂[N1,K1,T1 . (N1,K1)] from BINOP_1:sch 3(A9);
GT1 c= nextcard (predecessor M) ;
then GT1 c= M by Def17;
then bool GT1 c= bool M by ZFMISC_1:67;
then reconsider T = T1 as Function of [:(predecessor M),M:],(bool M) by FUNCT_2:7;
take T ; :: thesis:
A11: for N1, N2 being Element of predecessor M
for K1, K2 being Element of M
for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H₁(N1,K4) = K1 & H₁(N2,K4) = K2 )

proof

let N1, N2 be Element of predecessor M; :: thesis:
let K1, K2 be Element of M; :: thesis:
let K3 be set ; :: thesis:
defpred S₃[ Element of GT1] means H₁(N1,$1) = K1;
defpred S₄[ Element of GT1] means H₁(N2,$1) = K2;
assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; :: thesis:
then A13: K3 in T1 . (N1,K1) by XBOOLE_0:def 4;
then reconsider K4 = K3 as Element of GT1 ;
take K4 ; :: thesis:
thus K4 = K3 ; :: thesis:
A14: K4 in { K5 where K5 is Element of GT1 : S₃[K5] } by A10, A13;
thus S₃[K4] from CARD_FIL:sch 1(A14); :: thesis:
K3 in T1 . (N2,K2) by A12, XBOOLE_0:def 4;
then A15: K4 in { K5 where K5 is Element of GT1 : S₄[K5] } by A10;
thus S₄[K4] from CARD_FIL:sch 1(A15); :: thesis:

end;

thus for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty :: according to CARD_FIL:def 18 :: thesis:

proof

let N1 be Element of predecessor M; :: thesis:
let K1, K2 be Element of M; :: thesis:
assume A16: K1 <> K2 ; :: thesis:
assume not (T . (N1,K1)) /\ (T . (N1,K2)) is empty ; :: thesis:
then consider K3 being object such that
A17: K3 in (T . (N1,K1)) /\ (T . (N1,K2)) ;
ex K4 being Element of GT1 st
( K4 = K3 & H₁(N1,K4) = K1 & H₁(N1,K4) = K2 ) by A11, A17;
hence contradiction by A16; :: thesis:

end;

thus for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty :: thesis:

proof

let K1 be Element of M; :: thesis:
let N1, N2 be Element of predecessor M; :: thesis:
assume A18: N1 <> N2 ; :: thesis:
assume not (T . (N1,K1)) /\ (T . (N2,K1)) is empty ; :: thesis:
then consider K3 being object such that
A19: K3 in (T . (N1,K1)) /\ (T . (N2,K1)) ;
consider K4 being Element of GT1 such that
K4 = K3 and
A20: ( H₁(N1,K4) = K1 & H₁(N2,K4) = K1 ) by A11, A19;
ex f being Function st
( h1 . K4 = f & f is one-to-one & dom f = predecessor M & rng f = K4 ) by A8;
hence contradiction by A18, A20; :: thesis:

end;

A21: for N1 being Element of predecessor M
for K1 being Element of GT1 holds
( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

proof

let N1 be Element of predecessor M; :: thesis:
let K1 be Element of GT1; :: thesis:
ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A8;
hence ( dom (h . K1) = predecessor M & rng (h . K1) = K1 ) ; :: thesis:

end;

thus for N1 being Element of predecessor M holds card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M :: thesis:

proof

let N1 be Element of predecessor M; :: thesis:
union { (T . (N1,K1)) where K1 is Element of M : K1 in M } = GT1

proof

for S1 being set st S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } holds
S1 c= GT1

proof

let S1 be set ; :: thesis:
assume S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } ; :: thesis:
then consider K1 being Element of M such that
A22: S1 = T . (N1,K1) and
K1 in M ;
T1 . (N1,K1) c= GT1 ;
hence S1 c= GT1 by A22; :: thesis:

end;

hence union { (T . (N1,K1)) where K1 is Element of M : K1 in M } c= GT1 by ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis:
let K2 be object ; :: according to TARSKI:def 3 :: thesis:
assume A23: K2 in GT1 ; :: thesis:
reconsider K5 = K2 as Element of GT1 by A23;
N1 in predecessor M ;
then N1 in dom (h . K5) by A21;
then (h . K5) . N1 in rng (h . K5) by FUNCT_1:def 3;
then A24: H₁(N1,K5) in K5 by A21;
K2 in nextcard (predecessor M) by A23;
then K2 in M by Def17;
then A25: K5 c= M by ORDINAL1:def 2;
then A26: T . (N1,H₁(N1,K5)) in { (T . (N1,K1)) where K1 is Element of M : K1 in M } by A24;
K5 in { K3 where K3 is Element of GT1 : H₁(N1,K3) = H₁(N1,K5) } ;
then K5 in T . (N1,H₁(N1,K5)) by A10, A25, A24;
hence K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } by A26, TARSKI:def 4; :: thesis:

end;

then union { (T . (N1,K1)) where K1 is Element of M : K1 in M } = M \ (predecessor M) by Def17;
then M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } ) = M /\ (predecessor M) by XBOOLE_1:48;
hence card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M by CARD_1:7, XBOOLE_1:17; :: thesis:

end;

thus for K1 being Element of M holds card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M :: thesis:

proof

let K1 be Element of M; :: thesis:
A27: ( predecessor M c= K1 implies card K1 = predecessor M )

proof

assume predecessor M c= K1 ; :: thesis:
then card (predecessor M) c= card K1 by CARD_1:11;
then A28: predecessor M c= card K1 ;
card K1 in M by CARD_1:9;
then card K1 in nextcard (predecessor M) by Def17;
then card K1 c= predecessor M by CARD_3:91;
hence card K1 = predecessor M by A28; :: thesis:

end;

A29: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M

proof

per cases by ORDINAL1:16;

suppose A30: predecessor M c= K1 ; :: thesis:

M \ (K1 \/ {K1}) c= { K5 where K5 is Element of GT1 : K1 in K5 }

proof

let K6 be object ; :: according to TARSKI:def 3 :: thesis:
assume A31: K6 in M \ (K1 \/ {K1}) ; :: thesis:
reconsider K7 = K6 as Element of M by A31;
A32: not K6 in K1 \/ {K1} by A31, XBOOLE_0:def 5;
then not K6 in {K1} by XBOOLE_0:def 3;
then A33: not K6 = K1 by TARSKI:def 1;
K7 in M ;
then A34: K7 in nextcard (predecessor M) by Def17;
not K6 in K1 by A32, XBOOLE_0:def 3;
then A35: K1 in K7 by A33, ORDINAL1:14;
then predecessor M in K7 by A30, ORDINAL1:12;
then reconsider K8 = K7 as Element of GT1 by A34, XBOOLE_0:def 5;
K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A35;
hence K6 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis:

end;

then M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M \ (M \ (K1 \/ {K1})) by XBOOLE_1:34;
then A36: M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M /\ (K1 \/ {K1}) by XBOOLE_1:48;
not K1 is finite by A30;
then A37: card (K1 \/ {K1}) = card K1 by CARD_2:78;
M /\ (K1 \/ {K1}) c= K1 \/ {K1} by XBOOLE_1:17;
then M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= K1 \/ {K1} by A36;
hence card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M by A27, A30, A37, CARD_1:11; :: thesis:

end;

suppose A38: K1 in predecessor M ; :: thesis:

{ K5 where K5 is Element of GT1 : K1 in K5 } = GT1

proof

defpred S₃[ set ] means K1 in $1;
{ K5 where K5 is Element of GT1 : S₃[K5] } is Subset of GT1 from DOMAIN_1:sch 7();
hence { K5 where K5 is Element of GT1 : K1 in K5 } c= GT1 ; :: according to XBOOLE_0:def 10 :: thesis:
let K6 be object ; :: according to TARSKI:def 3 :: thesis:
assume A39: K6 in GT1 ; :: thesis:
reconsider K7 = K6 as Element of nextcard (predecessor M) by A39;
reconsider K8 = K7 as Element of GT1 by A39;
not K6 in predecessor M by A39, XBOOLE_0:def 5;
then predecessor M c= K7 by ORDINAL1:16;
then K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A38;
hence K6 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis:

end;

then M \ { K5 where K5 is Element of GT1 : K1 in K5 } = M \ (M \ (predecessor M)) by Def17
.= M /\ (predecessor M) by XBOOLE_1:48 ;
hence card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M by CARD_1:7, XBOOLE_1:17; :: thesis:

end;

{ K5 where K5 is Element of GT1 : K1 in K5 } c= union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M }

proof

let K4 be object ; :: according to TARSKI:def 3 :: thesis:
assume K4 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis:
then consider K5 being Element of GT1 such that
A40: K4 = K5 and
A41: K1 in K5 ;
rng (h . K5) = K5 by A21;
then consider N2 being object such that
A42: N2 in dom (h . K5) and
A43: (h . K5) . N2 = K1 by A41, FUNCT_1:def 3;
reconsider N3 = N2 as Element of predecessor M by A21, A42;
K5 in { K3 where K3 is Element of GT1 : H₁(N3,K3) = K1 } by A43;
then A44: K5 in T . (N3,K1) by A10;
T . (N3,K1) in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ;
hence K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } by A40, A44, TARSKI:def 4; :: thesis:

end;

then M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ) c= M \ { K5 where K5 is Element of GT1 : K1 in K5 } by XBOOLE_1:34;
then card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) by CARD_1:11;
hence card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A29; :: thesis:

end;