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

proof

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

end;

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

proof

let K1 be set ; :: thesis:
assume A8: K1 in dom h1 ; :: thesis:
consider f being Function such that
A9: ( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A6, A7, A8;
thus h1 . K1 is Function by A9; :: 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:32;
then reconsider GT1 = (nextcard (predecessor M)) \ (predecessor M) as non empty set by XBOOLE_0:def 5;
A10: 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:
consider f being Function such that
A11: ( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A7;
thus ( dom (h . K1) = predecessor M & rng (h . K1) = K1 ) by A11; :: thesis:

end;

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 } ;
A12: 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;
A13: { K2 where K2 is Element of GT1 : S₃[K2] } is Subset of GT1 from DOMAIN_1:sch 7();
take { K2 where K2 is Element of GT1 : H₁(N1,K2) = K1 } ; :: thesis:
thus ( { 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 } ] ) by A13; :: thesis:

end;

consider T1 being Function of [:(predecessor M),M:],(bool GT1) such that
A14: 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(A12);
GT1 c= nextcard (predecessor M) ;
then GT1 c= M by Def17;
then bool GT1 c= bool M by ZFMISC_1:79;
then reconsider T = T1 as Function of [:(predecessor M),M:],(bool M) by FUNCT_2:9;
take T ; :: thesis:
A15: 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:
assume K3 in (T . N1,K1) /\ (T . N2,K2) ; :: thesis:
then A16: ( K3 in T1 . N1,K1 & K3 in T1 . N2,K2 ) by XBOOLE_0:def 4;
then reconsider K4 = K3 as Element of GT1 ;
take K4 ; :: thesis:
thus K4 = K3 ; :: thesis:
defpred S₃[ Element of GT1] means H₁(N1,$1) = K1;
defpred S₄[ Element of GT1] means H₁(N2,$1) = K2;
A17: K4 in { K5 where K5 is Element of GT1 : S₃[K5] } by A14, A16;
A18: K4 in { K5 where K5 is Element of GT1 : S₄[K5] } by A14, A16;
thus S₃[K4] from CARD_FIL:sch 1(A17); :: thesis:
thus S₄[K4] from CARD_FIL:sch 1(A18); :: 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 A19: K1 <> K2 ; :: thesis:
assume not (T . N1,K1) /\ (T . N1,K2) is empty ; :: thesis:
then consider K3 being set such that
A20: K3 in (T . N1,K1) /\ (T . N1,K2) by XBOOLE_0:def 1;
consider K4 being Element of GT1 such that
A21: ( K4 = K3 & H₁(N1,K4) = K1 & H₁(N1,K4) = K2 ) by A15, A20;
thus contradiction by A19, A21; :: 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 A22: N1 <> N2 ; :: thesis:
assume not (T . N1,K1) /\ (T . N2,K1) is empty ; :: thesis:
then consider K3 being set such that
A23: K3 in (T . N1,K1) /\ (T . N2,K1) by XBOOLE_0:def 1;
consider K4 being Element of GT1 such that
A24: ( K4 = K3 & H₁(N1,K4) = K1 & H₁(N2,K4) = K1 ) by A15, A23;
consider f being Function such that
A25: ( h1 . K4 = f & f is one-to-one & dom f = predecessor M & rng f = K4 ) by A7;
thus contradiction by A22, A24, A25, FUNCT_1:def 8; :: 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 A26: S1 in { (T . N1,K1) where K1 is Element of M : K1 in M } ; :: thesis:
consider K1 being Element of M such that
A27: ( S1 = T . N1,K1 & K1 in M ) by A26;
T1 . N1,K1 c= GT1 ;
hence S1 c= GT1 by A27; :: thesis:

end;

hence union { (T . N1,K1) where K1 is Element of M : K1 in M } c= GT1 by ZFMISC_1:94; :: according to XBOOLE_0:def 10 :: thesis:
let K2 be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: K2 in GT1 ; :: thesis:
K2 in nextcard (predecessor M) by A28;
then K2 in M by Def17;
then A29: K2 c= M by ORDINAL1:def 2;
reconsider K5 = K2 as Element of GT1 by A28;
N1 in predecessor M ;
then N1 in dom (h . K5) by A10;
then (h . K5) . N1 in rng (h . K5) by FUNCT_1:def 5;
then A30: H₁(N1,K5) in K5 by A10;
K5 in { K3 where K3 is Element of GT1 : H₁(N1,K3) = H₁(N1,K5) } ;
then A31: K5 in T . N1,H₁(N1,K5) by A14, A29, A30;
T . N1,H₁(N1,K5) in { (T . N1,K1) where K1 is Element of M : K1 in M } by A29, A30;
hence K2 in union { (T . N1,K1) where K1 is Element of M : K1 in M } by A31, 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:23, 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:
A32: { 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A33: K4 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis:
consider K5 being Element of GT1 such that
A34: K4 = K5 and
A35: K1 in K5 by A33;
rng (h . K5) = K5 by A10;
then consider N2 being set such that
A36: ( N2 in dom (h . K5) & (h . K5) . N2 = K1 ) by A35, FUNCT_1:def 5;
reconsider N3 = N2 as Element of predecessor M by A10, A36;
K5 in { K3 where K3 is Element of GT1 : H₁(N3,K3) = K1 } by A36;
then A37: K5 in T . N3,K1 by A14;
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 A34, A37, TARSKI:def 4; :: thesis:

end;

A38: ( 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:27;
then A39: predecessor M c= card K1 by CARD_1:def 5;
card K1 in M by CARD_1:25;
then card K1 in nextcard (predecessor M) by Def17;
then card K1 c= predecessor M by CARD_3:108;
hence card K1 = predecessor M by A39, XBOOLE_0:def 10; :: thesis:

end;

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

proof

per cases by ORDINAL1:26;

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

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

proof

let K6 be set ; :: according to TARSKI:def 3 :: thesis:
assume A42: K6 in M \ (K1 \/ {K1}) ; :: thesis:
( K6 in M & not K6 in K1 \/ {K1} ) by A42, XBOOLE_0:def 5;
then ( not K6 in {K1} & not K6 in K1 ) by XBOOLE_0:def 3;
then A43: ( not K6 = K1 & not K6 in K1 ) by TARSKI:def 1;
reconsider K7 = K6 as Element of M by A42;
K7 in M ;
then A44: K7 in nextcard (predecessor M) by Def17;
A45: K1 in K7 by A43, ORDINAL1:24;
then predecessor M in K7 by A41, ORDINAL1:22;
then reconsider K8 = K7 as Element of GT1 by A44, XBOOLE_0:def 5;
K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A45;
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 A46: M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M /\ (K1 \/ {K1}) by XBOOLE_1:48;
M /\ (K1 \/ {K1}) c= K1 \/ {K1} by XBOOLE_1:17;
then A47: M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= K1 \/ {K1} by A46, XBOOLE_1:1;
not K1 is finite by A41;
then card (K1 \/ {K1}) = card K1 by CARD_3:120;
hence card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M by A38, A41, A47, CARD_1:27; :: thesis:

end;

suppose A48: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A49: K6 in GT1 ; :: thesis:
A50: ( K6 in nextcard (predecessor M) & not K6 in predecessor M ) by A49, XBOOLE_0:def 5;
reconsider K7 = K6 as Element of nextcard (predecessor M) by A49;
A51: predecessor M c= K7 by A50, ORDINAL1:26;
reconsider K8 = K7 as Element of GT1 by A49;
K8 in { K5 where K5 is Element of GT1 : K1 in K5 } by A48, A51;
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:23, XBOOLE_1:17; :: thesis:

end;

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 A32, 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:27;
hence card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A40, XBOOLE_1:1; :: thesis:

end;