let MySigmaField, MySet be set ; :: thesis: for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} holds
Intersection A1 in MySigmaField
let A1 be SetSequence of MySet; :: thesis: ( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} & Intersection A1 <> {} implies Intersection A1 in MySigmaField )
assume A0: ( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} ) ; :: thesis: ( not Intersection A1 <> {} or Intersection A1 in MySigmaField )
assume A5: Intersection A1 <> {} ; :: thesis: Intersection A1 in MySigmaField
D1: dom A1 = NAT by FUNCT_2:def 1;
A4: for n being Nat holds
( A1 . n = {} or A1 . n = {1,2,3,4} )
proof
let n be Nat; :: thesis: ( A1 . n = {} or A1 . n = {1,2,3,4} )
A1 . n in MySigmaField
proof
n in dom A1 by D1, ORDINAL1:def 12;
hence A1 . n in MySigmaField by FUNCT_1:3, A0; :: thesis: verum
end;
hence ( A1 . n = {} or A1 . n = {1,2,3,4} ) by A0, TARSKI:def 2; :: thesis: verum
end;
H1: ( ex n being Nat st A1 . n = {} implies Intersection A1 = {} )
proof
assume ex n being Nat st A1 . n = {} ; :: thesis: Intersection A1 = {}
then for x being object holds
( x in Intersection A1 iff x in {} ) by PROB_1:13;
hence Intersection A1 = {} by TARSKI:def 3; :: thesis: verum
end;
Intersection A1 = {1,2,3,4}
proof
for x being object holds
( x in Intersection A1 iff x in {1,2,3,4} )
proof
let x be object ; :: thesis: ( x in Intersection A1 iff x in {1,2,3,4} )
( x in Intersection A1 iff for n being Nat holds x in {1,2,3,4} )
proof
thus ( x in Intersection A1 implies for n being Nat holds x in {1,2,3,4} ) :: thesis: ( ( for n being Nat holds x in {1,2,3,4} ) implies x in Intersection A1 )
proof
assume G1: x in Intersection A1 ; :: thesis: for n being Nat holds x in {1,2,3,4}
for n being Nat holds x in {1,2,3,4}
proof
let n be Nat; :: thesis: x in {1,2,3,4}
for x being object holds
( x in A1 . n iff x in {1,2,3,4} ) by H1, A4, A5;
hence x in {1,2,3,4} by PROB_1:13, G1; :: thesis: verum
end;
hence for n being Nat holds x in {1,2,3,4} ; :: thesis: verum
end;
assume G1: for n being Nat holds x in {1,2,3,4} ; :: thesis: x in Intersection A1
for n being Nat holds x in A1 . n
proof
let n be Nat; :: thesis: x in A1 . n
x in {1,2,3,4} by G1;
hence x in A1 . n by H1, A4, A5; :: thesis: verum
end;
hence x in Intersection A1 by PROB_1:13; :: thesis: verum
end;
hence ( x in Intersection A1 iff x in {1,2,3,4} ) ; :: thesis: verum
end;
hence Intersection A1 = {1,2,3,4} by TARSKI:def 3; :: thesis: verum
end;
hence Intersection A1 in MySigmaField by A0, TARSKI:def 2; :: thesis: verum