let M be non limit_cardinal Aleph; :: thesis: for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds

ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

set N = predecessor M;

let I be Ideal of M; :: thesis: ( I is_complete_with M & Frechet_Ideal M c= I implies ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) ) )

assume that

A1: I is_complete_with M and

A2: Frechet_Ideal M c= I ; :: thesis: ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

consider T being Inf_Matrix of (predecessor M),M,(bool M) such that

A3: T is_Ulam_Matrix_of M by Th34;

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

A16: for K1 being Element of M holds S_{1}[K1,h . K1]
from FUNCT_2:sch 3(A8);

ex N2 being Element of predecessor M st card (h " {N2}) = M

A20: card (h " {N2}) = M ;

{ (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } c= bool 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)

h . (f . X) = N2

A38: for K1, K2 being Element of M st h . K1 = N2 & K1 <> K2 holds

T . (N2,K1) <> T . (N2,K2)

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

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: ( ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

thus for X1 being set st X1 in S holds

not X1 in I :: thesis: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2

X1 misses X2 :: thesis: verum

ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

set N = predecessor M;

let I be Ideal of M; :: thesis: ( I is_complete_with M & Frechet_Ideal M c= I implies ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) ) )

assume that

A1: I is_complete_with M and

A2: Frechet_Ideal M c= I ; :: thesis: ex S being Subset-Family of M st

( card S = M & ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

consider T being Inf_Matrix of (predecessor M),M,(bool M) such that

A3: T is_Ulam_Matrix_of M by Th34;

defpred S

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

A8:
for K1 being Element of M ex N2 being Element of predecessor M st S
deffunc H_{1}( Element of predecessor M, Element of M) -> Element of bool M = T . ($1,$2);

defpred S_{2}[ set , set ] means $1 in predecessor M;

let K1 be Element of M; :: thesis: union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I

defpred S_{3}[ set , set ] means ( $2 = K1 & $1 in predecessor M );

A6: { H_{1}(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : ( K2 = K1 & S_{2}[N1,K2] ) } = { H_{1}(N2,K1) where N2 is Element of predecessor M : S_{2}[N2,K1] }
from FRAENKEL:sch 20();

{ H_{1}(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : S_{3}[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: contradiction

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

end;defpred S

let K1 be Element of M; :: thesis: union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I

defpred S

A6: { H

{ H

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

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

proof

consider h being Function of M,(predecessor M) such that
deffunc H_{1}( set ) -> set = T . $1;

let K1 be Element of M; :: thesis: ex N2 being Element of predecessor M st S_{1}[K1,N2]

A9: not { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is empty_{1}(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}:] }

assume A13: for N2 being Element of predecessor M holds T . (N2,K1) in I ; :: thesis: contradiction

A14: { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= I

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

end;let K1 be Element of M; :: thesis: ex N2 being Element of predecessor M st S

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

proof

A10:
card { H
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: verum

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

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

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

assume Y in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis: Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] }

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

end;assume Y in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis: Y in { (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:] }

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

assume A13: for N2 being Element of predecessor M holds T . (N2,K1) in I ; :: thesis: contradiction

A14: { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= I

proof

card [:(predecessor M),{K1}:] = card (predecessor M)
by CARD_1:69;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } or X in I )

assume X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis: X in I

then ex N2 being Element of predecessor M st

( X = T . (N2,K1) & N2 in predecessor M ) ;

hence X in I by A13; :: thesis: verum

end;assume X in { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } ; :: thesis: X in I

then ex N2 being Element of predecessor M st

( X = T . (N2,K1) & N2 in predecessor M ) ;

hence X in I by A13; :: thesis: verum

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

A16: for K1 being Element of M holds S

ex N2 being Element of predecessor M st card (h " {N2}) = M

proof

then consider N2 being Element of predecessor M such that
deffunc H_{1}( set ) -> set = sup (h " {$1});

assume A17: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; :: thesis: contradiction

A18: { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= M_{1}(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 }

hence contradiction by ORDINAL2:19, SETWISEO:7; :: thesis: verum

end;assume A17: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; :: thesis: contradiction

A18: { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } c= M

proof

card { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } or x in M )

assume x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } ; :: thesis: x in M

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

end;assume x in { (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M } ; :: thesis: x in M

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

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

then
sup (h " {(h . K1)}) in K1
;
let N2 be Element of predecessor M; :: thesis: sup (h " {N2}) in sup { (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M }

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

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

hence contradiction by ORDINAL2:19, SETWISEO:7; :: thesis: verum

A20: card (h " {N2}) = M ;

{ (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } c= bool M

proof

then reconsider S = { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } as Subset-Family of M ;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } or X in bool M )

assume X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } ; :: thesis: X in bool M

then ex K2 being Element of M st

( X = T . (N2,K2) & h . K2 = N2 ) ;

hence X in bool M ; :: thesis: verum

end;assume X in { (T . (N2,K2)) where K2 is Element of M : h . K2 = N2 } ; :: thesis: X in bool M

then ex K2 being Element of M st

( X = T . (N2,K2) & h . K2 = N2 ) ;

hence X in bool M ; :: thesis: verum

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

A33:
for X being set st X in dom f holds
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in S or X in rng (G * f) )

assume X in S ; :: thesis: X in rng (G * f)

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

end;assume X in S ; :: thesis: X in rng (G * f)

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

h . (f . X) = N2

proof

rng (G * f) c= S
let X be set ; :: thesis: ( X in dom f implies h . (f . X) = N2 )

assume X in dom f ; :: thesis: h . (f . X) = N2

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

end;assume X in dom f ; :: thesis: h . (f . X) = N2

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

proof

then A37:
rng (G * f) = S
by A27;
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in rng (G * f) or X in S )

assume X in rng (G * f) ; :: thesis: X in S

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

end;assume X in rng (G * f) ; :: thesis: X in S

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

A38: for K1, K2 being Element of M st h . K1 = N2 & K1 <> K2 holds

T . (N2,K1) <> T . (N2,K2)

proof

A41:
G * f is one-to-one
let K1, K2 be Element of M; :: thesis: ( h . K1 = N2 & K1 <> K2 implies T . (N2,K1) <> T . (N2,K2) )

assume that

A39: h . K1 = N2 and

A40: K1 <> K2 ; :: thesis: T . (N2,K1) <> T . (N2,K2)

assume T . (N2,K1) = T . (N2,K2) ; :: thesis: contradiction

then (T . (N2,K1)) /\ (T . (N2,K2)) <> {} by A16, A39, Th11;

hence contradiction by A3, A40; :: thesis: verum

end;assume that

A39: h . K1 = N2 and

A40: K1 <> K2 ; :: thesis: T . (N2,K1) <> T . (N2,K2)

assume T . (N2,K1) = T . (N2,K2) ; :: thesis: contradiction

then (T . (N2,K1)) /\ (T . (N2,K2)) <> {} by A16, A39, Th11;

hence contradiction by A3, A40; :: thesis: verum

proof

take
S
; :: thesis: ( card S = M & ( for X1 being set st X1 in S holds
let K1, K2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not K1 in dom (G * f) or not K2 in dom (G * f) or not (G * f) . K1 = (G * f) . K2 or K1 = K2 )

assume that

A42: K1 in dom (G * f) and

A43: K2 in dom (G * f) and

A44: (G * f) . K1 = (G * f) . K2 ; :: thesis: K1 = K2

assume K1 <> K2 ; :: thesis: contradiction

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

end;assume that

A42: K1 in dom (G * f) and

A43: K2 in dom (G * f) and

A44: (G * f) . K1 = (G * f) . K2 ; :: thesis: K1 = K2

assume K1 <> K2 ; :: thesis: contradiction

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

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

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: ( ( for X1 being set st X1 in S holds

not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2 ) )

thus for X1 being set st X1 in S holds

not X1 in I :: thesis: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds

X1 misses X2

proof

thus
for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
let X1 be set ; :: thesis: ( X1 in S implies not X1 in I )

assume X1 in S ; :: thesis: not X1 in I

then ex K1 being Element of M st

( T . (N2,K1) = X1 & h . K1 = N2 ) ;

hence not X1 in I by A16; :: thesis: verum

end;assume X1 in S ; :: thesis: not X1 in I

then ex K1 being Element of M st

( T . (N2,K1) = X1 & h . K1 = N2 ) ;

hence not X1 in I by A16; :: thesis: verum

X1 misses X2 :: thesis: verum

proof

let X1, X2 be set ; :: thesis: ( X1 in S & X2 in S & X1 <> X2 implies X1 misses X2 )

assume that

A50: X1 in S and

A51: X2 in S and

A52: X1 <> X2 ; :: thesis: X1 misses X2

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

end;assume that

A50: X1 in S and

A51: X2 in S and

A52: X1 <> X2 ; :: thesis: X1 misses X2

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