let M be non limit_cardinal Aleph; :: thesis:
set N = predecessor M;
let I be Ideal of M; :: thesis:
assume that
A1: I is_complete_with M and
A2: Frechet_Ideal M c= I ; :: thesis:
consider T being Inf_Matrix of (predecessor M),M,(bool M) such that
A3: T is_Ulam_Matrix_of M by Th34;
defpred S₁[ set , set ] means not T . ($2,$1) in I;
A4: M = nextcard (predecessor M) by Def17;
A5: for K1 being Element of M holds union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I

proof

deffunc H₁( Element of predecessor M, Element of M) -> Element of bool M = T . ($1,$2);
defpred S₂[ set , set ] means $1 in predecessor M;
let K1 be Element of M; :: thesis:
defpred S₃[ set , set ] means ( $2 = K1 & $1 in predecessor M );
A6: { H₁(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : ( K2 = K1 & S₂[N1,K2] ) } = { H₁(N2,K1) where N2 is Element of predecessor M : S₂[N2,K1] } from FRAENKEL:sch 20();
{ H₁(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : S₃[N1,K2] } is Subset-Family of M from DOMAIN_1:sch 9();
then reconsider C = { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } as Subset-Family of M by A6;
assume not union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I ; :: thesis:
then not (union C) ` in Frechet_Ideal M by A2, SETFAM_1:def 7;
then not card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) in card M by Th19;
then A7: not card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) in nextcard (predecessor M) by A4;
card (M \ (union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A3;
hence contradiction by A7, CARD_3:91; :: thesis:

end;

A8: for K1 being Element of M ex N2 being Element of predecessor M st S₁[K1,N2]

proof

deffunc H₁( set ) -> set = T . $1;
let K1 be Element of M; :: thesis:
A9: not { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is empty

proof

set N2 = the Element of predecessor M;
T . ( the Element of predecessor M,K1) in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ;
hence not { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is empty ; :: thesis:

end;

A10: card { H₁(X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } c= card [:(predecessor M),{K1}:] from TREES_2:sch 2();
{ (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] }

proof

let Y be object ; :: according to TARSKI:def 3 :: thesis:
assume Y in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis:
then consider N1 being Element of predecessor M such that
A11: Y = T . (N1,K1) and
N1 in predecessor M ;
( [N1,K1] is Element of [:(predecessor M),M:] & [N1,K1] in [:(predecessor M),{K1}:] ) by ZFMISC_1:87, ZFMISC_1:106;
hence Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } by A11; :: thesis:

end;

then A12: card { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= card { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } by CARD_1:11;
assume A13: for N2 being Element of predecessor M holds T . (N2,K1) in I ; :: thesis:
A14: { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= I

proof

let X be object ; :: according to TARSKI:def 3 :: thesis:
assume X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis:
then ex N2 being Element of predecessor M st
( X = T . (N2,K1) & N2 in predecessor M ) ;
hence X in I by A13; :: thesis:

end;

card [:(predecessor M),{K1}:] = card (predecessor M) by CARD_1:69;
then A15: card [:(predecessor M),{K1}:] = predecessor M ;
predecessor M in M by A4, CARD_1:18;
then card { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in M by A10, A12, A15, ORDINAL1:12, XBOOLE_1:1;
then union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in I by A1, A14, A9;
hence contradiction by A5, Th10; :: thesis:

end;

consider h being Function of M,(predecessor M) such that
A16: for K1 being Element of M holds S₁[K1,h . K1] from FUNCT_2:sch 3(A8);
ex N2 being Element of predecessor M st card (h " {N2}) = M

proof

deffunc H₁( set ) -> set = sup (h " {$1});
assume A17: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; :: thesis:
A18: { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } ; :: thesis:
then consider N2 being Element of predecessor M such that
A19: x = sup (h " {N2}) and
N2 in predecessor M ;
( card (h " {N2}) c= M & card (h " {N2}) <> M ) by A17, CARD_1:7;
then card (h " {N2}) in M by CARD_1:3;
then card (h " {N2}) in cf M by CARD_5:def 3;
hence x in M by A19, CARD_5:26; :: thesis:

end;

card { H₁(N2) where N2 is Element of predecessor M : N2 in predecessor M } c= card (predecessor M) from TREES_2:sch 2();
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= predecessor M ;
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in M by A4, CARD_3:91;
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in cf M by CARD_5:def 3;
then reconsider K1 = sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } as Element of M by A18, CARD_5:26;
for N2 being Element of predecessor M holds sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M }

proof

let N2 be Element of predecessor M; :: thesis:
sup (h " {N2}) in { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } ;
hence sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } by ORDINAL2:19; :: thesis:

end;

then sup (h " {(h . K1)}) in K1 ;
hence contradiction by ORDINAL2:19, SETWISEO:7; :: thesis:

end;

then consider N2 being Element of predecessor M such that
A20: card (h " {N2}) = M ;
{ (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } c= bool M

proof

let X be object ; :: according to TARSKI:def 3 :: thesis:
assume X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } ; :: thesis:
then ex K2 being Element of M st
( X = T . (N2,K2) & h . K2 = N2 ) ;
hence X in bool M ; :: thesis:

end;

then reconsider S = { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } as Subset-Family of M ;
dom T = [:(predecessor M),M:] by FUNCT_2:def 1;
then consider G being Function such that
(curry T) . N2 = G and
A21: dom G = M and
rng G c= rng T and
A22: for y being object st y in M holds
G . y = T . (N2,y) by FUNCT_5:29;
h " {N2},M are_equipotent by A20, CARD_1:def 2;
then consider f being Function such that
A23: f is one-to-one and
A24: dom f = M and
A25: rng f = h " {N2} by WELLORD2:def 4;
A26: dom (G * f) = dom f by A25, A21, RELAT_1:27;
A27: S c= rng (G * f)

proof

let X be object ; :: according to TARSKI:def 3 :: thesis:
assume X in S ; :: thesis:
then consider K2 being Element of M such that
A28: X = T . (N2,K2) and
A29: h . K2 = N2 ;
K2 in M ;
then A30: K2 in dom h by FUNCT_2:def 1;
h . K2 in {N2} by A29, TARSKI:def 1;
then K2 in h " {N2} by A30, FUNCT_1:def 7;
then consider K3 being object such that
A31: K3 in dom f and
A32: f . K3 = K2 by A25, FUNCT_1:def 3;
X = G . (f . K3) by A22, A28, A32;
then X = (G * f) . K3 by A26, A31, FUNCT_1:12;
hence X in rng (G * f) by A26, A31, FUNCT_1:def 3; :: thesis:

end;

A33: for X being set st X in dom f holds
h . (f . X) = N2

proof

let X be set ; :: thesis:
assume X in dom f ; :: thesis:
then f . X in h " {N2} by A25, FUNCT_1:def 3;
then h . (f . X) in {N2} by FUNCT_1:def 7;
hence h . (f . X) = N2 by TARSKI:def 1; :: thesis:

end;

rng (G * f) c= S

proof

let X be object ; :: according to TARSKI:def 3 :: thesis:
assume X in rng (G * f) ; :: thesis:
then consider K1 being object such that
A34: K1 in dom (G * f) and
A35: X = (G * f) . K1 by FUNCT_1:def 3;
f . K1 in rng f by A26, A34, FUNCT_1:def 3;
then reconsider K3 = f . K1 as Element of M by A25;
X = G . (f . K1) by A34, A35, FUNCT_1:12;
then A36: X = T . (N2,K3) by A22;
h . K3 = N2 by A33, A26, A34;
hence X in S by A36; :: thesis:

end;

then A37: rng (G * f) = S by A27;
A38: for K1, K2 being Element of M st h . K1 = N2 & K1 <> K2 holds
T . (N2,K1) <> T . (N2,K2)

proof

let K1, K2 be Element of M; :: thesis:
assume that
A39: h . K1 = N2 and
A40: K1 <> K2 ; :: thesis:
assume T . (N2,K1) = T . (N2,K2) ; :: thesis:
then (T . (N2,K1)) /\ (T . (N2,K2)) <> {} by A16, A39, Th11;
hence contradiction by A3, A40; :: thesis:

end;

A41: G * f is one-to-one

proof

let K1, K2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A42: K1 in dom (G * f) and
A43: K2 in dom (G * f) and
A44: (G * f) . K1 = (G * f) . K2 ; :: thesis:
assume K1 <> K2 ; :: thesis:
then A45: f . K1 <> f . K2 by A23, A26, A42, A43;
A46: f . K2 in rng f by A26, A43, FUNCT_1:def 3;
then reconsider K4 = f . K2 as Element of M by A25;
A47: (G * f) . K2 = G . (f . K2) by A43, FUNCT_1:12
.= T . (N2,(f . K2)) by A25, A22, A46 ;
A48: f . K1 in rng f by A26, A42, FUNCT_1:def 3;
then reconsider K3 = f . K1 as Element of M by A25;
h . K3 = N2 by A33, A26, A42;
then A49: T . (N2,K3) <> T . (N2,K4) by A38, A45;
(G * f) . K1 = G . (f . K1) by A42, FUNCT_1:12
.= T . (N2,(f . K1)) by A25, A22, A48 ;
hence contradiction by A44, A49, A47; :: thesis:

end;

take S ; :: thesis:
dom (G * f) = M by A24, A25, A21, RELAT_1:27;
then S,M are_equipotent by A37, A41, WELLORD2:def 4;
hence card S = M by CARD_1:def 2; :: thesis:
thus for X1 being set st X1 in S holds
not X1 in I :: thesis:

proof

let X1 be set ; :: thesis:
assume X1 in S ; :: thesis:
then ex K1 being Element of M st
( T . (N2,K1) = X1 & h . K1 = N2 ) ;
hence not X1 in I by A16; :: thesis:

end;

thus for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 :: thesis:

proof

let X1, X2 be set ; :: thesis:
assume that
A50: X1 in S and
A51: X2 in S and
A52: X1 <> X2 ; :: thesis:
consider K2 being Element of M such that
A53: T . (N2,K2) = X2 and
h . K2 = N2 by A51;
consider K1 being Element of M such that
A54: T . (N2,K1) = X1 and
h . K1 = N2 by A50;
(T . (N2,K1)) /\ (T . (N2,K2)) = {} by A3, A52, A54, A53;
hence X1 misses X2 by A54, A53; :: thesis:

end;