let M be non limit_cardinal Aleph; :: thesis:
set N = predecessor M;
A1: M = nextcard (predecessor M) by Def17;
let I be Ideal of M; :: thesis:
assume that
A2: I is_complete_with M and
A3: Frechet_Ideal M c= I ; :: thesis:
consider T being Inf_Matrix of (predecessor M),M,(bool M) such that
A4: T is_Ulam_Matrix_of M by Th34;
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

let K1 be Element of M; :: thesis:
defpred S₁[ set , set ] means ( $2 = K1 & $1 in predecessor M );
defpred S₂[ set , set ] means $1 in predecessor M;
deffunc H₁( Element of predecessor M, Element of M) -> Element of bool M = T . $1,$2;
A6: { 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();
{ 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();
then reconsider C = { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } as Subset-Family of M by A6;
A7: card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M by A4, Def18;
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 A3, SETFAM_1:def 8;
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 not card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) in nextcard (predecessor M) by A1, CARD_1:def 5;
hence contradiction by A7, CARD_3:108; :: thesis:

end;

defpred S₁[ set , set ] means not T . $2,$1 in I;
A8: for K1 being Element of M ex N2 being Element of predecessor M st S₁[K1,N2]

proof

let K1 be Element of M; :: thesis:
assume A9: for N2 being Element of predecessor M holds T . N2,K1 in I ; :: thesis:
A10: { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } c= I

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume A11: X in { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis:
consider N2 being Element of predecessor M such that
A12: X = T . N2,K1 and
N2 in predecessor M by A11;
thus X in I by A9, A12; :: thesis:

end;

A13: not { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } is empty

proof

consider N2 being Element of predecessor M;
T . N2,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;

A14: predecessor M in M by A1, CARD_1:32;
deffunc H₁( set ) -> set = T . $1;
A15: 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 set ; :: according to TARSKI:def 3 :: thesis:
assume A16: Y in { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis:
consider N1 being Element of predecessor M such that
A17: ( Y = T . N1,K1 & N1 in predecessor M ) by A16;
( [N1,K1] is Element of [:(predecessor M),M:] & [N1,K1] in [:(predecessor M),{K1}:] ) by ZFMISC_1:106, ZFMISC_1:129;
hence Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] } by A17; :: thesis:

end;

then A18: 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:27;
card [:(predecessor M),{K1}:] = card (predecessor M) by CARD_2:13;
then card [:(predecessor M),{K1}:] = predecessor M by CARD_1:def 5;
then card { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } in M by A14, A15, A18, ORDINAL1:22, XBOOLE_1:1;
then union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } in I by A2, A10, A13, Def4;
hence contradiction by A5, Th10; :: thesis:

end;

consider h being Function of M,(predecessor M) such that
A20: 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

assume A21: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; :: thesis:
A22: { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= M

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } ; :: thesis:
consider N2 being Element of predecessor M such that
A24: ( x = sup (h " {N2}) & N2 in predecessor M ) by A23;
( card (h " {N2}) c= M & card (h " {N2}) <> M ) by A21, CARD_1:23;
then card (h " {N2}) in M by CARD_1:13;
then card (h " {N2}) in cf M by CARD_5:def 4;
hence x in M by A24, CARD_5:38; :: thesis:

end;

deffunc H₁( set ) -> set = sup (h " {$1});
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 by CARD_1:def 5;
then card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in M by A1, CARD_3:108;
then A25: card { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } in cf M by CARD_5:def 4;
A26: 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:27; :: thesis:

end;

reconsider K1 = sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M } as Element of M by A22, A25, CARD_5:38;
sup (h " {(h . K1)}) in K1 by A26;
hence contradiction by ORDINAL2:27, SETWISEO:12; :: thesis:

end;

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

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: X in { (T . N2,K2) where K2 is Element of M : h . K2 = N2 } ; :: thesis:
consider K2 being Element of M such that
A29: ( X = T . N2,K2 & h . K2 = N2 ) by A28;
thus X in bool M by A29; :: thesis:

end;

then reconsider S = { (T . N2,K2) where K2 is Element of M : h . K2 = N2 } as Subset-Family of M ;
take S ; :: thesis:
A30: 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 A31: ( h . K1 = N2 & K1 <> K2 ) ; :: thesis:
assume T . N2,K1 = T . N2,K2 ; :: thesis:
then (T . N2,K1) /\ (T . N2,K2) <> {} by A20, A31, Th11;
hence contradiction by A4, A31, Def18; :: thesis:

end;

h " {N2},M are_equipotent by A27, CARD_1:def 5;
then consider f being Function such that
A32: ( f is one-to-one & dom f = M & rng f = h " {N2} ) by WELLORD2:def 4;
A33: for X being set st X in dom f holds
h . (f . X) = N2

proof

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

end;

dom T = [:(predecessor M),M:] by FUNCT_2:def 1;
then consider G being Function such that
(curry T) . N2 = G and
A35: ( dom G = M & rng G c= rng T ) and
A36: for y being set st y in M holds
G . y = T . N2,y by FUNCT_5:36;
A37: dom (G * f) = M by A32, A35, RELAT_1:46;
A38: dom (G * f) = dom f by A32, A35, RELAT_1:46;
A39: rng (G * f) = S

proof

thus rng (G * f) c= S :: according to XBOOLE_0:def 10 :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume A40: X in rng (G * f) ; :: thesis:
consider K1 being set such that
A41: ( K1 in dom (G * f) & X = (G * f) . K1 ) by A40, FUNCT_1:def 5;
f . K1 in rng f by A38, A41, FUNCT_1:def 5;
then reconsider K3 = f . K1 as Element of M by A32;
A42: h . K3 = N2 by A33, A38, A41;
X = G . (f . K1) by A41, FUNCT_1:22;
then X = T . N2,K3 by A36;
hence X in S by A42; :: thesis:

end;

thus S c= rng (G * f) :: thesis:

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume A43: X in S ; :: thesis:
consider K2 being Element of M such that
A44: ( X = T . N2,K2 & h . K2 = N2 ) by A43;
A45: h . K2 in {N2} by A44, TARSKI:def 1;
K2 in M ;
then K2 in dom h by FUNCT_2:def 1;
then K2 in h " {N2} by A45, FUNCT_1:def 13;
then consider K3 being set such that
A46: ( K3 in dom f & f . K3 = K2 ) by A32, FUNCT_1:def 5;
X = G . (f . K3) by A36, A44, A46;
then X = (G * f) . K3 by A38, A46, FUNCT_1:22;
hence X in rng (G * f) by A38, A46, FUNCT_1:def 5; :: thesis:

end;

G * f is one-to-one

proof

let K1, K2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A47: ( K1 in dom (G * f) & K2 in dom (G * f) ) and
A48: (G * f) . K1 = (G * f) . K2 ; :: thesis:
A49: ( f . K1 in rng f & f . K2 in rng f ) by A38, A47, FUNCT_1:def 5;
assume K1 <> K2 ; :: thesis:
then A50: f . K1 <> f . K2 by A32, A38, A47, FUNCT_1:def 8;
reconsider K3 = f . K1 as Element of M by A32, A49;
A51: h . K3 = N2 by A33, A38, A47;
reconsider K4 = f . K2 as Element of M by A32, A49;
A52: T . N2,K3 <> T . N2,K4 by A30, A50, A51;
A53: (G * f) . K1 = G . (f . K1) by A47, FUNCT_1:22
.= T . N2,(f . K1) by A32, A36, A49 ;
(G * f) . K2 = G . (f . K2) by A47, FUNCT_1:22
.= T . N2,(f . K2) by A32, A36, A49 ;
hence contradiction by A48, A52, A53; :: thesis:

end;

then S,M are_equipotent by A37, A39, WELLORD2:def 4;
hence card S = M by CARD_1:def 5; :: thesis:
thus for X1 being set st X1 in S holds
not X1 in I :: thesis:

proof

let X1 be set ; :: thesis:
assume A54: X1 in S ; :: thesis:
consider K1 being Element of M such that
A55: T . N2,K1 = X1 and
A56: h . K1 = N2 by A54;
thus not X1 in I by A20, A55, A56; :: 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 A57: ( X1 in S & X2 in S & X1 <> X2 ) ; :: thesis:
consider K1 being Element of M such that
A58: T . N2,K1 = X1 and
h . K1 = N2 by A57;
consider K2 being Element of M such that
A59: T . N2,K2 = X2 and
h . K2 = N2 by A57;
(T . N2,K1) /\ (T . N2,K2) = {} by A4, A57, A58, A59, Def18;
hence X1 misses X2 by A58, A59, XBOOLE_0:def 7; :: thesis:

end;