let X1, X2 be set ; :: thesis: for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A be Subset-Family of [:X1,X2:]; :: thesis: for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A1 be non empty Subset-Family of X1; :: thesis: for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]
let A2 be non empty Subset-Family of X2; :: thesis: ( A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } implies Intersect A = [:(Intersect A1),(Intersect A2):] )
assume A1: A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } ; :: thesis: Intersect A = [:(Intersect A1),(Intersect A2):]
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:(Intersect A1),(Intersect A2):] c= Intersect A
let x be object ; :: thesis: ( x in Intersect A implies x in [:(Intersect A1),(Intersect A2):] )
assume A2: x in Intersect A ; :: thesis: x in [:(Intersect A1),(Intersect A2):]
then consider x1, x2 being object such that
A3: x1 in X1 and
A4: x2 in X2 and
A5: [x1,x2] = x by ZFMISC_1:def 2;
set a1 = the Element of A1;
set a2 = the Element of A2;
reconsider a1 = the Element of A1 as Subset of X1 ;
reconsider a2 = the Element of A2 as Subset of X2 ;
now :: thesis: for a being set st a in A1 holds
x1 in a
let a be set ; :: thesis: ( a in A1 implies x1 in a )
assume a in A1 ; :: thesis: x1 in a
then [:a,a2:] in A by A1;
then x in [:a,a2:] by A2, SETFAM_1:43;
hence x1 in a by A5, ZFMISC_1:87; :: thesis: verum
end;
then A6: x1 in Intersect A1 by A3, SETFAM_1:43;
now :: thesis: for a being set st a in A2 holds
x2 in a
let a be set ; :: thesis: ( a in A2 implies x2 in a )
assume a in A2 ; :: thesis: x2 in a
then [:a1,a:] in A by A1;
then x in [:a1,a:] by A2, SETFAM_1:43;
hence x2 in a by A5, ZFMISC_1:87; :: thesis: verum
end;
then x2 in Intersect A2 by A4, SETFAM_1:43;
hence x in [:(Intersect A1),(Intersect A2):] by A5, A6, ZFMISC_1:87; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [:(Intersect A1),(Intersect A2):] or x in Intersect A )
assume A7: x in [:(Intersect A1),(Intersect A2):] ; :: thesis: x in Intersect A
then consider x1, x2 being object such that
A8: x1 in Intersect A1 and
A9: x2 in Intersect A2 and
A10: [x1,x2] = x by ZFMISC_1:def 2;
now :: thesis: for c being set st c in A holds
x in c
let c be set ; :: thesis: ( c in A implies x in c )
assume c in A ; :: thesis: x in c
then consider a being Subset of X1, b being Subset of X2 such that
A11: c = [:a,b:] and
A12: a in A1 and
A13: b in A2 by A1;
A14: x1 in a by A8, A12, SETFAM_1:43;
x2 in b by A9, A13, SETFAM_1:43;
hence x in c by A10, A11, A14, ZFMISC_1:87; :: thesis: verum
end;
hence x in Intersect A by A7, SETFAM_1:43; :: thesis: verum