let A1 be SetSequence of {1,2,3,4}; ( ( 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}} )
; ( 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;
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;
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;
( 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;
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 MYSUPP0:
Intersection A1 <> {1,2,3,4}
;
( 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}
;
( 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 ;
( 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
;
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;
verum
end;
hence
( ( for
n being
Nat holds
x in A1 . n ) iff
x in {1,2,3,4} )
by ASS1;
verum
end;
hence
(
x in Intersection A1 iff
x in {1,2,3,4} )
by PROB_1:13;
verum
end;
hence
Intersection A1 = {1,2,3,4}
by TARSKI:2;
verum
end; hence
(
Intersection A1 = {} or
Intersection A1 = {1,2} or
Intersection A1 = {3,4} )
by MYSUPP0;
verum end; end;
end;
hence
(
Intersection A1 c= {} or
Intersection A1 c= {1,2} or
Intersection A1 c= {3,4} )
;
verum
end; end; end;