let X1, X2 be non empty set ; for S1 being with_countable_Cover Subset-Family of X1
for S2 being with_countable_Cover Subset-Family of X2
for S being Subset-Family of [:X1,X2:] st S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } holds
S is with_countable_Cover
let S1 be with_countable_Cover Subset-Family of X1; for S2 being with_countable_Cover Subset-Family of X2
for S being Subset-Family of [:X1,X2:] st S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } holds
S is with_countable_Cover
let S2 be with_countable_Cover Subset-Family of X2; for S being Subset-Family of [:X1,X2:] st S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } holds
S is with_countable_Cover
let S be Subset-Family of [:X1,X2:]; ( S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } implies S is with_countable_Cover )
assume A1:
S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) }
; S is with_countable_Cover
ex U being countable Subset of S st
( union U = [:X1,X2:] & U is Subset of S )
proof
consider U1 being
countable Subset of
S1 such that A2:
U1 is
Cover of
X1
by SRINGS_1:def 4;
A3:
union U1 = X1
by A2, Lem6a;
consider U2 being
countable Subset of
S2 such that A4:
U2 is
Cover of
X2
by SRINGS_1:def 4;
A5:
union U2 = X2
by A4, Lem6a;
set U =
{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } ;
A6:
not
U1 is
empty
by A2, ZFMISC_1:2, Lem6a;
A7:
not
U1 \ {{}} is
empty
A8:
not
U2 is
empty
by A4, Lem6a, ZFMISC_1:2;
A9:
not
U2 \ {{}} is
empty
set V =
{ [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ;
A10:
{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } = { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) }
{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } is
Subset of
S
proof
for
x being
object st
x in { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } holds
x in S
proof
let x be
object ;
( x in { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } implies x in S )
assume
x in { u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) }
;
x in S
then consider u0 being
Subset of
[:X1,X2:] such that A11:
(
x = u0 & ex
u1,
u2 being
set st
(
u1 in U1 \ {{}} &
u2 in U2 \ {{}} &
u0 = [:u1,u2:] ) )
;
reconsider x =
x as
Subset of
[:X1,X2:] by A11;
thus
x in S
by A1, A11;
verum
end;
hence
{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } is
Subset of
S
by TARSKI:def 3;
verum
end;
then reconsider U =
{ u where u is Subset of [:X1,X2:] : ex u1, u2 being set st
( u1 in U1 \ {{}} & u2 in U2 \ {{}} & u = [:u1,u2:] ) } as
Subset of
S ;
A12:
U is
countable
proof
(
U1 \ {{}} is
countable &
U2 \ {{}} is
countable )
by CARD_3:95;
then A13:
[:(U1 \ {{}}),(U2 \ {{}}):] is
countable
by CARD_4:7;
set W =
[:(U1 \ {{}}),(U2 \ {{}}):];
{ [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ,
[:(U1 \ {{}}),(U2 \ {{}}):] are_equipotent
proof
set Z =
{ [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ;
A14:
( ( for
v being
object st
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex
w being
object st
(
w in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
w being
object st
w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex
v being
object st
(
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
v1,
v2,
w1,
w2 being
object st
[v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } &
[v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
(
v1 = v2 iff
w1 = w2 ) ) )
proof
A15:
for
v being
object st
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex
w being
object st
(
w in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
proof
let v be
object ;
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } implies ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) )
assume
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) }
;
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
then consider u1 being
Element of
U1 such that A16:
ex
u2 being
Element of
U2 st
(
v = [:u1,u2:] &
u1 in U1 \ {{}} &
u2 in U2 \ {{}} )
;
consider u2 being
Element of
U2 such that A17:
(
v = [:u1,u2:] &
u1 in U1 \ {{}} &
u2 in U2 \ {{}} )
by A16;
set w =
[u1,u2];
take
[u1,u2]
;
( [u1,u2] in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,[u1,u2]] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
thus
(
[u1,u2] in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,[u1,u2]] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
by A17, ZFMISC_1:def 2;
verum
end;
A18:
for
w being
object st
w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex
v being
object st
(
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
proof
let w be
object ;
( w in [:(U1 \ {{}}),(U2 \ {{}}):] implies ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) )
assume
w in [:(U1 \ {{}}),(U2 \ {{}}):]
;
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
then
ex
u1,
u2 being
object st
(
u1 in U1 \ {{}} &
u2 in U2 \ {{}} &
w = [u1,u2] )
by ZFMISC_1:def 2;
then consider u1,
u2 being
set such that A19:
(
w = [u1,u2] &
u1 in U1 \ {{}} &
u2 in U2 \ {{}} )
;
set v =
[:u1,u2:];
take
[:u1,u2:]
;
( [:u1,u2:] in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [[:u1,u2:],w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
(
u1 is
Element of
U1 &
u2 is
Element of
U2 )
by A19, XBOOLE_1:36, TARSKI:def 3;
hence
(
[:u1,u2:] in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[[:u1,u2:],w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } )
by A19;
verum
end;
for
v1,
v2,
w1,
w2 being
object st
[v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } &
[v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
(
v1 = v2 iff
w1 = w2 )
proof
let v1,
v2,
w1,
w2 be
object ;
( [v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } implies ( v1 = v2 iff w1 = w2 ) )
assume
[v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) }
;
( not [v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } or ( v1 = v2 iff w1 = w2 ) )
then consider a1 being
Element of
U1,
a2 being
Element of
U2 such that A21:
(
[v1,w1] = [[:a1,a2:],[a1,a2]] &
a1 in U1 \ {{}} &
a2 in U2 \ {{}} )
;
A22:
(
v1 = [:a1,a2:] &
w1 = [a1,a2] )
by A21, XTUPLE_0:1;
assume
[v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) }
;
( v1 = v2 iff w1 = w2 )
then consider b1 being
Element of
U1,
b2 being
Element of
U2 such that A23:
(
[v2,w2] = [[:b1,b2:],[b1,b2]] &
b1 in U1 \ {{}} &
b2 in U2 \ {{}} )
;
A24:
(
v2 = [:b1,b2:] &
w2 = [b1,b2] )
by A23, XTUPLE_0:1;
thus
(
v1 = v2 implies
w1 = w2 )
( w1 = w2 implies v1 = v2 )
assume A26:
w1 = w2
;
v1 = v2
(
w1 = [a1,a2] &
w2 = [b1,b2] )
by A21, A23, XTUPLE_0:1;
then
(
a1 = b1 &
a2 = b2 )
by A26, XTUPLE_0:1;
hence
v1 = v2
by A21, A23, XTUPLE_0:1;
verum
end;
hence
( ( for
v being
object st
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex
w being
object st
(
w in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
w being
object st
w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex
v being
object st
(
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
v1,
v2,
w1,
w2 being
object st
[v1,w1] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } &
[v2,w2] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
(
v1 = v2 iff
w1 = w2 ) ) )
by A15, A18;
verum
end;
ex
Z being
set st
( ( for
v being
object st
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex
w being
object st
(
w in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,w] in Z ) ) & ( for
w being
object st
w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex
v being
object st
(
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[v,w] in Z ) ) & ( for
x,
y,
z,
u being
object st
[x,y] in Z &
[z,u] in Z holds
(
x = z iff
y = u ) ) )
proof
take
{ [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) }
;
( ( for v being object st v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex w being object st
( w in [:(U1 \ {{}}),(U2 \ {{}}):] & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for w being object st w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex v being object st
( v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } & [v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for x, y, z, u being object st [x,y] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } & [z,u] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
( x = z iff y = u ) ) )
thus
( ( for
v being
object st
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } holds
ex
w being
object st
(
w in [:(U1 \ {{}}),(U2 \ {{}}):] &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
w being
object st
w in [:(U1 \ {{}}),(U2 \ {{}}):] holds
ex
v being
object st
(
v in { [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } &
[v,w] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } ) ) & ( for
x,
y,
z,
u being
object st
[x,y] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } &
[z,u] in { [[:u1,u2:],[u1,u2]] where u1 is Element of U1, u2 is Element of U2 : ( u1 in U1 \ {{}} & u2 in U2 \ {{}} ) } holds
(
x = z iff
y = u ) ) )
by A14;
verum
end;
hence
{ [:a,b:] where a is Element of U1, b is Element of U2 : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ,
[:(U1 \ {{}}),(U2 \ {{}}):] are_equipotent
;
verum
end;
hence
U is
countable
by A10, A13, YELLOW_8:4;
verum
end;
union U = [:X1,X2:]
proof
set V2 =
{ [:a,b:] where a is Element of U1 \ {{}}, b is Element of U2 \ {{}} : ( a in U1 \ {{}} & b in U2 \ {{}} ) } ;
A26:
U = { [:a,b:] where a is Element of U1 \ {{}}, b is Element of U2 \ {{}} : ( a in U1 \ {{}} & b in U2 \ {{}} ) }
(
union (U1 \ {{}}) = union U1 &
union (U2 \ {{}}) = union U2 )
by PARTIT1:2;
hence
union U = [:X1,X2:]
by A3, A5, A7, A9, A26, LATTICE5:2;
verum
end;
hence
ex
U being
countable Subset of
S st
(
union U = [:X1,X2:] &
U is
Subset of
S )
by A12;
verum
end;
hence
S is with_countable_Cover
by Lem6a, SRINGS_1:def 4; verum