let A, B be non empty set ; [:(union A),(union B):] = union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
set Y = { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } ;
thus
[:(union A),(union B):] c= union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
XBOOLE_0:def 10 union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } c= [:(union A),(union B):]proof
let z be
object ;
TARSKI:def 3 ( not z in [:(union A),(union B):] or z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } )
assume A1:
z in [:(union A),(union B):]
;
z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
then consider x,
y being
object such that A2:
z = [x,y]
by RELAT_1:def 1;
y in union B
by A1, A2, ZFMISC_1:87;
then consider b9 being
set such that A3:
y in b9
and A4:
b9 in B
by TARSKI:def 4;
x in union A
by A1, A2, ZFMISC_1:87;
then consider a9 being
set such that A5:
x in a9
and A6:
a9 in A
by TARSKI:def 4;
reconsider b9 =
b9 as
Element of
B by A4;
reconsider a9 =
a9 as
Element of
A by A6;
A7:
[:a9,b9:] in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
;
z in [:a9,b9:]
by A2, A5, A3, ZFMISC_1:def 2;
hence
z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
by A7, TARSKI:def 4;
verum
end;
let z be object ; TARSKI:def 3 ( not z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } or z in [:(union A),(union B):] )
assume
z in union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
; z in [:(union A),(union B):]
then consider e being set such that
A8:
z in e
and
A9:
e in { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
by TARSKI:def 4;
consider a9 being Element of A, b9 being Element of B such that
A10:
[:a9,b9:] = e
and
a9 in A
and
b9 in B
by A9;
consider x, y being object such that
A11:
( x in a9 & y in b9 )
and
A12:
z = [x,y]
by A8, A10, ZFMISC_1:def 2;
( x in union A & y in union B )
by A11, TARSKI:def 4;
hence
z in [:(union A),(union B):]
by A12, ZFMISC_1:def 2; verum