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 S1[ 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))) & S1[K1,x] )
proof
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))) & S1[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))) & S1[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))) & S1[K1,x] ) by A4, A5, A6; :: thesis: verum
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
S1[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: ( 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;
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 H1( set , set ) -> set = (h . $2) . $1;
defpred S2[ set , set , set ] means $3 = { K2 where K2 is Element of GT1 : H1($1,K2) = $2 } ;
A9: for N1 being Element of predecessor M
for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
proof
let N1 be Element of predecessor M; :: thesis: for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
let K1 be Element of M; :: thesis: ex S1 being Subset of GT1 st S2[N1,K1,S1]
defpred S3[ set ] means H1(N1,$1) = K1;
take { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ; :: thesis: ( { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } is Subset of GT1 & S2[N1,K1, { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ] )
{ K2 where K2 is Element of GT1 : S3[K2] } is Subset of GT1 from DOMAIN_1:sch 7();
 hence ( { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } is Subset of GT1 & S2[N1,K1, { K2 where K2 is Element of GT1 : H1(N1,K2) = K1 } ] ) ; :: thesis: verum
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 S2[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 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
proof
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 & H1(N1,K4) = K1 & H1(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 & H1(N1,K4) = K1 & H1(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 & H1(N1,K4) = K1 & H1(N2,K4) = K2 ) )
defpred S3[ Element of GT1] means H1(N1,$1) = K1;
defpred S4[ Element of GT1] means H1(N2,$1) = K2;
assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; :: thesis: ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(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 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
thus K4 = K3 ; :: thesis: ( H1(N1,K4) = K1 & H1(N2,K4) = K2 )
A14: K4 in { K5 where K5 is Element of GT1 : S3[K5] } by A10, A13;
thus S3[K4] from CARD_FIL:sch 1(A14); :: thesis: H1(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 : S4[K5] } by A10;
thus S4[K4] from CARD_FIL:sch 1(A15); :: thesis: verum
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: ( ( 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
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 & H1(N1,K4) = K1 & H1(N1,K4) = K2 ) by A11, A17;
hence contradiction by A16; :: thesis: verum
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: ( ( 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
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: ( H1(N1,K4) = K1 & H1(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;
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: 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;
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
proof
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
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: ( 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;
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 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: H1(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,H1(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 : H1(N1,K3) = H1(N1,K5) } ;
then K5 in T . (N1,H1(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;
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: verum
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: 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 )
proof
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;
A29: card (M \ { K5 where K5 is Element of GT1 : K1 in K5 } ) c= predecessor M
proof
per cases ( predecessor M c= K1 or K1 in predecessor M ) by ORDINAL1:16;
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 }
proof
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;
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: verum
end;
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
proof
defpred S3[ set ] means K1 in $1;
{ K5 where K5 is Element of GT1 : S3[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;
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: verum
end;
end;
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: ( 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 : H1(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;
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: verum
end;