let X, Y be set ; for A being SetSequence of X
for B being SetSequence of Y
for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let A be SetSequence of X; for B being SetSequence of Y
for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let B be SetSequence of Y; for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
let C be SetSequence of [:X,Y:]; ( A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) implies ( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] ) )
assume that
A1:
A is non-descending
and
A2:
B is non-descending
and
A3:
for n being Nat holds C . n = [:(A . n),(B . n):]
; ( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
for n, m being Nat st n <= m holds
C . n c= C . m
hence
C is non-descending
by PROB_1:def 5; ( C is convergent & Union C = [:(Union A),(Union B):] )
hence
C is convergent
by SETLIM_1:63; Union C = [:(Union A),(Union B):]
now for z being set st z in [:(Union A),(Union B):] holds
z in Union Clet z be
set ;
( z in [:(Union A),(Union B):] implies z in Union C )assume
z in [:(Union A),(Union B):]
;
z in Union Cthen consider x,
y being
object such that A6:
(
x in Union A &
y in Union B &
z = [x,y] )
by ZFMISC_1:def 2;
A7:
(
x in union (rng A) &
y in union (rng B) )
by A6, CARD_3:def 4;
then consider A1 being
set such that A8:
(
x in A1 &
A1 in rng A )
by TARSKI:def 4;
consider n being
object such that A9:
(
n in dom A &
A1 = A . n )
by A8, FUNCT_1:def 3;
reconsider n =
n as
Nat by A9;
consider B1 being
set such that A10:
(
y in B1 &
B1 in rng B )
by A7, TARSKI:def 4;
consider m being
object such that A11:
(
m in dom B &
B1 = B . m )
by A10, FUNCT_1:def 3;
reconsider m =
m as
Nat by A11;
reconsider N =
max (
n,
m) as
Element of
NAT by ORDINAL1:def 12;
(
A . n c= A . N &
B . m c= B . N )
by A1, A2, XXREAL_0:25, PROB_1:def 5;
then
z in [:(A . N),(B . N):]
by A6, A8, A9, A10, A11, ZFMISC_1:def 2;
then
(
z in C . N &
C . N in rng C )
by A3, FUNCT_2:112;
then
z in union (rng C)
by TARSKI:def 4;
hence
z in Union C
by CARD_3:def 4;
verum end;
then A12:
[:(Union A),(Union B):] c= Union C
;
now for z being set st z in Union C holds
z in [:(Union A),(Union B):]let z be
set ;
( z in Union C implies z in [:(Union A),(Union B):] )assume
z in Union C
;
z in [:(Union A),(Union B):]then
z in union (rng C)
by CARD_3:def 4;
then consider C1 being
set such that A13:
(
z in C1 &
C1 in rng C )
by TARSKI:def 4;
consider n being
object such that A14:
(
n in dom C &
C1 = C . n )
by A13, FUNCT_1:def 3;
reconsider n =
n as
Element of
NAT by A14;
z in [:(A . n),(B . n):]
by A3, A13, A14;
then consider x,
y being
object such that A15:
(
x in A . n &
y in B . n &
z = [x,y] )
by ZFMISC_1:def 2;
(
A . n in rng A &
B . n in rng B )
by FUNCT_2:112;
then
(
x in union (rng A) &
y in union (rng B) )
by A15, TARSKI:def 4;
then
(
x in Union A &
y in Union B )
by CARD_3:def 4;
hence
z in [:(Union A),(Union B):]
by A15, ZFMISC_1:def 2;
verum end;
then
Union C c= [:(Union A),(Union B):]
;
hence
Union C = [:(Union A),(Union B):]
by A12; verum