let A1 be SetSequence of {1,2,3,4}; :: thesis: ( ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} & not Intersection A1 = {} & not Intersection A1 = {1,2} & not Intersection A1 = {3,4} implies Intersection A1 = {1,2,3,4} )
assume GENASS0: ( ( for n, k being Nat holds not (A1 . n) /\ (A1 . k) = {} ) & rng A1 c= {{},{1,2},{3,4},{1,2,3,4}} ) ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
set MyOmega = {{},{1,2},{3,4},{1,2,3,4}};
D1: dom A1 = NAT by FUNCT_2:def 1;
S20: for n being Nat holds A1 . n in {{},{1,2},{3,4},{1,2,3,4}}
proof
let n be Nat; :: thesis: A1 . n in {{},{1,2},{3,4},{1,2,3,4}}
n in dom A1 by D1, ORDINAL1:def 12;
hence A1 . n in {{},{1,2},{3,4},{1,2,3,4}} by FUNCT_1:3, GENASS0; :: thesis: verum
end;
S2: for n being Nat holds
( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} )
proof
let n be Nat; :: thesis: ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} )
A1 . n in {{},{1,2},{3,4},{1,2,3,4}} by S20;
hence ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) by ENUMSET1:def 2; :: thesis: verum
end;
Fin1: for n being Nat holds Intersection A1 c= A1 . n by PROB_1:13;
per cases ( Intersection A1 = {1,2,3,4} or Intersection A1 <> {1,2,3,4} ) ;
suppose Intersection A1 = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum
end;
suppose MYSUPP0: Intersection A1 <> {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
W0: ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} )
proof
( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
proof
per cases ( for n being Nat holds A1 . n = {1,2,3,4} or ex n being Nat st A1 . n <> {1,2,3,4} ) ;
suppose ASS1: for n being Nat holds A1 . n = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
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} )
( ( for n being Nat holds x in A1 . n ) iff x in {1,2,3,4} )
proof
( ( for n being Nat holds x in A1 . n ) implies x in {1,2,3,4} )
proof
assume for n being Nat holds x in A1 . n ; :: thesis: x in {1,2,3,4}
then x in A1 . 0 ;
then consider k being Nat such that
N10: x in A1 . k ;
thus x in {1,2,3,4} by N10; :: thesis: verum
end;
hence ( ( for n being Nat holds x in A1 . n ) iff x in {1,2,3,4} ) by ASS1; :: thesis: verum
end;
hence ( x in Intersection A1 iff x in {1,2,3,4} ) by PROB_1:13; :: thesis: verum
end;
hence Intersection A1 = {1,2,3,4} by TARSKI:2; :: thesis: verum
end;
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by MYSUPP0; :: thesis: verum
end;
suppose ex n being Nat st A1 . n <> {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
then consider n being Nat such that
KK: A1 . n <> {1,2,3,4} ;
per cases ( A1 . n = {} or A1 . n = {1,2} or A1 . n = {3,4} or A1 . n = {1,2,3,4} ) by S2;
suppose A1 . n = {} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by The1; :: thesis: verum
end;
suppose JSUPP1: A1 . n = {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
( Intersection A1 = {} or Intersection A1 = {1,2} ) hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) ; :: thesis: verum
end;
suppose SUPP1: A1 . n = {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
( Intersection A1 = {} or Intersection A1 = {3,4} ) hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) ; :: thesis: verum
end;
suppose A1 . n = {1,2,3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} )
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} ) by KK; :: thesis: verum
end;
end;
end;
end;
end;
hence ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} ) ; :: thesis: verum
end;
per cases ( Intersection A1 c= {} or Intersection A1 c= {1,2} or Intersection A1 c= {3,4} ) by W0;
suppose Intersection A1 c= {} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
hence ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} ) ; :: thesis: verum
end;
suppose ZW10: Intersection A1 c= {1,2} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
end;
suppose ZW10: Intersection A1 c= {3,4} ; :: thesis: ( Intersection A1 = {} or Intersection A1 = {1,2} or Intersection A1 = {3,4} or Intersection A1 = {1,2,3,4} )
end;
end;
end;
end;