let M be non limit_cardinal Aleph; :: thesis: ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M

set N = predecessor M;

set GT = (nextcard (predecessor M)) \ (predecessor M);

defpred S_{1}[ 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_{1}[K1,x] )

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_{1}[K1,h1 . K1]
from FUNCT_1:sch 6(A1);

for K1 being object st K1 in dom h1 holds

h1 . K1 is Function

( 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_{1}( set , set ) -> set = (h . $2) . $1;

defpred S_{2}[ set , set , set ] means $3 = { K2 where K2 is Element of GT1 : H_{1}($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_{2}[N1,K1,S1]

A10: for N1 being Element of predecessor M

for K1 being Element of M holds S_{2}[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: T is_Ulam_Matrix_of M

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_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

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: ( ( 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 ) & ( 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 ) & ( 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 ) )

for N1, N2 being Element of predecessor M st N1 <> N2 holds

(T . (N1,K1)) /\ (T . (N2,K1)) is empty :: thesis: ( ( 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 ) & ( 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 ) )

for K1 being Element of GT1 holds

( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

set N = predecessor M;

set GT = (nextcard (predecessor M)) \ (predecessor M);

defpred S

( $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

proof

consider h1 being Function such that
let K1 be object ; :: thesis: ( K1 in (nextcard (predecessor M)) \ (predecessor M) implies ex x being object st

( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S_{1}[K1,x] ) )

assume A2: K1 in (nextcard (predecessor M)) \ (predecessor M) ; :: thesis: ex x being object st

( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S_{1}[K1,x] )

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_{1}[K1,x] )
by A4, A5, A6; :: thesis: verum

end;( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S

assume A2: K1 in (nextcard (predecessor M)) \ (predecessor M) ; :: thesis: ex x being object st

( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S

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

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

for K1 being object st K1 in dom h1 holds

h1 . K1 is Function

proof

then reconsider h = h1 as Function-yielding Function by FUNCOP_1:def 6;
let K1 be object ; :: thesis: ( K1 in dom h1 implies h1 . K1 is Function )

assume K1 in dom h1 ; :: thesis: h1 . K1 is Function

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: verum

end;assume K1 in dom h1 ; :: thesis: h1 . K1 is Function

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: verum

( 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

defpred S

A9: for N1 being Element of predecessor M

for K1 being Element of M ex S1 being Subset of GT1 st S

proof

consider T1 being Function of [:(predecessor M),M:],(bool GT1) such that
let N1 be Element of predecessor M; :: thesis: for K1 being Element of M ex S1 being Subset of GT1 st S_{2}[N1,K1,S1]

let K1 be Element of M; :: thesis: ex S1 being Subset of GT1 st S_{2}[N1,K1,S1]

defpred S_{3}[ set ] means H_{1}(N1,$1) = K1;

take { K2 where K2 is Element of GT1 : H_{1}(N1,K2) = K1 }
; :: thesis: ( { K2 where K2 is Element of GT1 : H_{1}(N1,K2) = K1 } is Subset of GT1 & S_{2}[N1,K1, { K2 where K2 is Element of GT1 : H_{1}(N1,K2) = K1 } ] )

{ K2 where K2 is Element of GT1 : S_{3}[K2] } is Subset of GT1
from DOMAIN_1:sch 7();

hence ( { K2 where K2 is Element of GT1 : H_{1}(N1,K2) = K1 } is Subset of GT1 & S_{2}[N1,K1, { K2 where K2 is Element of GT1 : H_{1}(N1,K2) = K1 } ] )
; :: thesis: verum

end;let K1 be Element of M; :: thesis: ex S1 being Subset of GT1 st S

defpred S

take { K2 where K2 is Element of GT1 : H

{ K2 where K2 is Element of GT1 : S

hence ( { K2 where K2 is Element of GT1 : H

A10: for N1 being Element of predecessor M

for K1 being Element of M holds S

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: T is_Ulam_Matrix_of M

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

proof

thus
for N1 being Element of predecessor M
let N1, N2 be Element of predecessor M; :: thesis: 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_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

let K1, K2 be Element of M; :: thesis: for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds

ex K4 being Element of GT1 st

( K4 = K3 & H_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

let K3 be set ; :: thesis: ( K3 in (T . (N1,K1)) /\ (T . (N2,K2)) implies ex K4 being Element of GT1 st

( K4 = K3 & H_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 ) )

defpred S_{3}[ Element of GT1] means H_{1}(N1,$1) = K1;

defpred S_{4}[ Element of GT1] means H_{1}(N2,$1) = K2;

assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; :: thesis: ex K4 being Element of GT1 st

( K4 = K3 & H_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

then A13: K3 in T1 . (N1,K1) by XBOOLE_0:def 4;

then reconsider K4 = K3 as Element of GT1 ;

take K4 ; :: thesis: ( K4 = K3 & H_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

thus K4 = K3 ; :: thesis: ( H_{1}(N1,K4) = K1 & H_{1}(N2,K4) = K2 )

A14: K4 in { K5 where K5 is Element of GT1 : S_{3}[K5] }
by A10, A13;

thus S_{3}[K4]
from CARD_FIL:sch 1(A14); :: thesis: H_{1}(N2,K4) = K2

K3 in T1 . (N2,K2) by A12, XBOOLE_0:def 4;

then A15: K4 in { K5 where K5 is Element of GT1 : S_{4}[K5] }
by A10;

thus S_{4}[K4]
from CARD_FIL:sch 1(A15); :: thesis: verum

end;for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds

ex K4 being Element of GT1 st

( K4 = K3 & H

let K1, K2 be Element of M; :: thesis: for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds

ex K4 being Element of GT1 st

( K4 = K3 & H

let K3 be set ; :: thesis: ( K3 in (T . (N1,K1)) /\ (T . (N2,K2)) implies ex K4 being Element of GT1 st

( K4 = K3 & H

defpred S

defpred S

assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; :: thesis: ex K4 being Element of GT1 st

( K4 = K3 & H

then A13: K3 in T1 . (N1,K1) by XBOOLE_0:def 4;

then reconsider K4 = K3 as Element of GT1 ;

take K4 ; :: thesis: ( K4 = K3 & H

thus K4 = K3 ; :: thesis: ( H

A14: K4 in { K5 where K5 is Element of GT1 : S

thus S

K3 in T1 . (N2,K2) by A12, XBOOLE_0:def 4;

then A15: K4 in { K5 where K5 is Element of GT1 : S

thus S

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: ( ( 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 ) & ( 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 ) & ( 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 ) )

proof

thus
for K1 being Element of M
let N1 be Element of predecessor M; :: thesis: for K1, K2 being Element of M st K1 <> K2 holds

(T . (N1,K1)) /\ (T . (N1,K2)) is empty

let K1, K2 be Element of M; :: thesis: ( K1 <> K2 implies (T . (N1,K1)) /\ (T . (N1,K2)) is empty )

assume A16: K1 <> K2 ; :: thesis: (T . (N1,K1)) /\ (T . (N1,K2)) is empty

assume not (T . (N1,K1)) /\ (T . (N1,K2)) is empty ; :: thesis: contradiction

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_{1}(N1,K4) = K1 & H_{1}(N1,K4) = K2 )
by A11, A17;

hence contradiction by A16; :: thesis: verum

end;(T . (N1,K1)) /\ (T . (N1,K2)) is empty

let K1, K2 be Element of M; :: thesis: ( K1 <> K2 implies (T . (N1,K1)) /\ (T . (N1,K2)) is empty )

assume A16: K1 <> K2 ; :: thesis: (T . (N1,K1)) /\ (T . (N1,K2)) is empty

assume not (T . (N1,K1)) /\ (T . (N1,K2)) is empty ; :: thesis: contradiction

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

hence contradiction by A16; :: thesis: verum

for N1, N2 being Element of predecessor M st N1 <> N2 holds

(T . (N1,K1)) /\ (T . (N2,K1)) is empty :: thesis: ( ( 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 ) & ( 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 ) )

proof

A21:
for N1 being Element of predecessor M
let K1 be Element of M; :: thesis: for N1, N2 being Element of predecessor M st N1 <> N2 holds

(T . (N1,K1)) /\ (T . (N2,K1)) is empty

let N1, N2 be Element of predecessor M; :: thesis: ( N1 <> N2 implies (T . (N1,K1)) /\ (T . (N2,K1)) is empty )

assume A18: N1 <> N2 ; :: thesis: (T . (N1,K1)) /\ (T . (N2,K1)) is empty

assume not (T . (N1,K1)) /\ (T . (N2,K1)) is empty ; :: thesis: contradiction

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_{1}(N1,K4) = K1 & H_{1}(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: verum

end;(T . (N1,K1)) /\ (T . (N2,K1)) is empty

let N1, N2 be Element of predecessor M; :: thesis: ( N1 <> N2 implies (T . (N1,K1)) /\ (T . (N2,K1)) is empty )

assume A18: N1 <> N2 ; :: thesis: (T . (N1,K1)) /\ (T . (N2,K1)) is empty

assume not (T . (N1,K1)) /\ (T . (N2,K1)) is empty ; :: thesis: contradiction

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

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: verum

for K1 being Element of GT1 holds

( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

proof

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: 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
let N1 be Element of predecessor M; :: thesis: for K1 being Element of GT1 holds

( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

let K1 be Element of GT1; :: thesis: ( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

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: verum

end;( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

let K1 be Element of GT1; :: thesis: ( dom (h . K1) = predecessor M & rng (h . K1) = K1 )

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: verum

proof

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: verum
let N1 be Element of predecessor M; :: thesis: card (M \ (union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )) c= predecessor M

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

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: verum

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

proof

then
union { (T . (N1,K1)) where K1 is Element of M : K1 in M } = M \ (predecessor M)
by Def17;
for S1 being set st S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } holds

S1 c= GT1

let K2 be object ; :: according to TARSKI:def 3 :: thesis: ( not K2 in GT1 or K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )

assume A23: K2 in GT1 ; :: thesis: K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M }

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_{1}(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_{1}(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_{1}(N1,K3) = H_{1}(N1,K5) }
;

then K5 in T . (N1,H_{1}(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: verum

end;S1 c= GT1

proof

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: GT1 c= union { (T . (N1,K1)) where K1 is Element of M : K1 in M }
let S1 be set ; :: thesis: ( S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } implies S1 c= GT1 )

assume S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } ; :: thesis: S1 c= GT1

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: verum

end;assume S1 in { (T . (N1,K1)) where K1 is Element of M : K1 in M } ; :: thesis: S1 c= GT1

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: verum

let K2 be object ; :: according to TARSKI:def 3 :: thesis: ( not K2 in GT1 or K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } )

assume A23: K2 in GT1 ; :: thesis: K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M }

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

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

K5 in { K3 where K3 is Element of GT1 : H

then K5 in T . (N1,H

hence K2 in union { (T . (N1,K1)) where K1 is Element of M : K1 in M } by A26, TARSKI:def 4; :: thesis: verum

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: verum

proof

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

A27: ( predecessor M c= K1 implies card K1 = predecessor M )

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: verum

end;A27: ( predecessor M c= K1 implies card K1 = predecessor M )

proof

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

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: verum

end;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: verum

proof
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 }
per cases
( predecessor M c= K1 or K1 in predecessor M )
by ORDINAL1:16;

end;

suppose A30:
predecessor M c= K1
; :: thesis: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M

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

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: verum

end;proof

then
M \ { K5 where K5 is Element of GT1 : K1 in K5 } c= M \ (M \ (K1 \/ {K1}))
by XBOOLE_1:34;
let K6 be object ; :: according to TARSKI:def 3 :: thesis: ( not K6 in M \ (K1 \/ {K1}) or K6 in { K5 where K5 is Element of GT1 : K1 in K5 } )

assume A31: K6 in M \ (K1 \/ {K1}) ; :: thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }

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: verum

end;assume A31: K6 in M \ (K1 \/ {K1}) ; :: thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }

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: verum

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: verum

suppose A38:
K1 in predecessor M
; :: thesis: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M

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

.= 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: verum

end;proof

then M \ { K5 where K5 is Element of GT1 : K1 in K5 } =
M \ (M \ (predecessor M))
by Def17
defpred S_{3}[ set ] means K1 in $1;

{ K5 where K5 is Element of GT1 : S_{3}[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: GT1 c= { K5 where K5 is Element of GT1 : K1 in K5 }

let K6 be object ; :: according to TARSKI:def 3 :: thesis: ( not K6 in GT1 or K6 in { K5 where K5 is Element of GT1 : K1 in K5 } )

assume A39: K6 in GT1 ; :: thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }

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: verum

end;{ K5 where K5 is Element of GT1 : S

hence { K5 where K5 is Element of GT1 : K1 in K5 } c= GT1 ; :: according to XBOOLE_0:def 10 :: thesis: GT1 c= { K5 where K5 is Element of GT1 : K1 in K5 }

let K6 be object ; :: according to TARSKI:def 3 :: thesis: ( not K6 in GT1 or K6 in { K5 where K5 is Element of GT1 : K1 in K5 } )

assume A39: K6 in GT1 ; :: thesis: K6 in { K5 where K5 is Element of GT1 : K1 in K5 }

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: verum

.= 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: verum

proof

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;
let K4 be object ; :: according to TARSKI:def 3 :: thesis: ( not K4 in { K5 where K5 is Element of GT1 : K1 in K5 } or K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )

assume K4 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis: K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M }

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_{1}(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: verum

end;assume K4 in { K5 where K5 is Element of GT1 : K1 in K5 } ; :: thesis: K4 in union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M }

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

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: verum

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: verum