let M be non limit_cardinal Aleph; 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; ( 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
; 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 S1[ 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 H1(
Element of
predecessor M,
Element of
M)
-> Element of
bool M =
T . ($1,$2);
defpred S2[
set ,
set ]
means $1
in predecessor M;
let K1 be
Element of
M;
union { (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } in dual I
defpred S3[
set ,
set ]
means ( $2
= K1 & $1
in predecessor M );
A6:
{ H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : ( K2 = K1 & S2[N1,K2] ) } = { H1(N2,K1) where N2 is Element of predecessor M : S2[N2,K1] }
from FRAENKEL:sch 20();
{ H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : S3[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
;
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;
verum
end;
A8:
for K1 being Element of M ex N2 being Element of predecessor M st S1[K1,N2]
proof
deffunc H1(
set )
-> set =
T . $1;
let K1 be
Element of
M;
ex N2 being Element of predecessor M st S1[K1,N2]
A9:
not
{ (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } is
empty
A10:
card { H1(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 ;
TARSKI:def 3 ( 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 }
;
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;
verum
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
;
contradiction
A14:
{ (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M } c= I
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;
verum
end;
consider h being Function of M,(predecessor M) such that
A16:
for K1 being Element of M holds S1[K1,h . K1]
from FUNCT_2:sch 3(A8);
ex N2 being Element of predecessor M st card (h " {N2}) = M
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
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 ;
TARSKI:def 3 ( not X in S or X in rng (G * f) )
assume
X in S
;
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;
verum
end;
A33:
for X being set st X in dom f holds
h . (f . X) = N2
rng (G * f) c= S
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;
( h . K1 = N2 & K1 <> K2 implies T . (N2,K1) <> T . (N2,K2) )
assume that A39:
h . K1 = N2
and A40:
K1 <> K2
;
T . (N2,K1) <> T . (N2,K2)
assume
T . (
N2,
K1)
= T . (
N2,
K2)
;
contradiction
then
(T . (N2,K1)) /\ (T . (N2,K2)) <> {}
by A16, A39, Th11;
hence
contradiction
by A3, A40;
verum
end;
A41:
G * f is one-to-one
proof
let K1,
K2 be
object ;
FUNCT_1:def 4 ( 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
;
K1 = K2
assume
K1 <> K2
;
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;
verum
end;
take
S
; ( 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 ) )
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; ( ( 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
for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2proof
let X1 be
set ;
( X1 in S implies not X1 in I )
assume
X1 in S
;
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;
verum
end;
thus
for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2
verum