let X1, X2, X3 be non empty set ; for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
let A1 be Subset of X1; for A2 being Subset of X2
for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
let A2 be Subset of X2; for A3 being Subset of X3 holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
let A3 be Subset of X3; [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
thus
[:A1,A2,A3:] c= { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
XBOOLE_0:def 10 { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } c= [:A1,A2,A3:]proof
let a be
object ;
TARSKI:def 3 ( not a in [:A1,A2,A3:] or a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } )
assume A1:
a in [:A1,A2,A3:]
;
a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
reconsider A1 =
A1 as non
empty Subset of
X1 by A1, MCART_1:31;
reconsider A2 =
A2 as non
empty Subset of
X2 by A1, MCART_1:31;
reconsider A3 =
A3 as non
empty Subset of
X3 by A1, MCART_1:31;
A2:
a in [:A1,A2,A3:]
by A1;
reconsider x =
a as
Element of
[:X1,X2,X3:] by A2;
A3:
x = [(x `1_3),(x `2_3),(x `3_3)]
;
A4:
x `3_3 in A3
by A2, MCART_1:72;
(
x `1_3 in A1 &
x `2_3 in A2 )
by A2, MCART_1:72;
hence
a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
by A4, A3;
verum
end;
let a be object ; TARSKI:def 3 ( not a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) } or a in [:A1,A2,A3:] )
assume
a in { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }
; a in [:A1,A2,A3:]
then
ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st
( a = [x1,x2,x3] & x1 in A1 & x2 in A2 & x3 in A3 )
;
hence
a in [:A1,A2,A3:]
by MCART_1:69; verum