environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve x,y,z,A,B,C,X,Y for set;
::2.107
for A,B holds A /\ B c= A & A /\ B c= B &
(for X st X c= A & X c= B holds X c= A /\ B)
proof
let A,B;
thus A /\ B c= A
proof
let x;
assume x in A /\ B;
hence x in A by ENUMSET:def 7;
end;
thus A /\ B c= B
proof
let x;
assume x in A /\ B;
hence x in B by ENUMSET:def 7;
end;
thus for X st X c= A & X c= B holds X c= A /\ B
proof
let X;
assume X: X c= A & X c= B;
thus X c= A/\B
proof
let x;
assume x in X;
then x in A & x in B by X,ENUMSET:def 10;
hence x in A/\B by ENUMSET:def 7;
end;
end;
end;
::2.108
for A,B holds A c= A\/B & B c= A\/B &
(for X st A c= X & B c= X holds A\/B c= X)
proof
let A,B;
thus A c= A\/B
proof
let x;
assume x in A;
hence x in A\/B by ENUMSET:def 6;
end;
thus B c= A\/B
proof
let x;
assume x in B;
hence x in A\/B by ENUMSET:def 6;
end;
thus for X st A c= X & B c= X holds A\/B c= X
proof
let X;
assume X: A c= X & B c= X;
thus A\/B c= X
proof
let x;
assume x in A\/B;
then x in A or x in B by ENUMSET:def 6;
hence x in X by X,ENUMSET:def 10;
end;
end;
end;
::2.109
for A,B holds A\B c= A & A\B misses B &
(for X st X c= A & X misses B holds X c= A\B)
proof
let A,B;
thus A\B c= A
proof
let x;
assume x in A\B;
hence x in A by ENUMSET:def 8;
end;
(A\B) /\ B = {}
proof
thus (A\B) /\ B c= {}
proof
let x;
assume x in (A\B) /\ B;
then x in A\B & x in B by ENUMSET:def 7;
then x in A & not x in B & x in B by ENUMSET:def 8;
hence x in {};
end;
thus {} c= (A\B) /\ B
proof
let x;
assume x in {};
hence x in (A\B) /\ B by ENUMSET:def 1;
end;
end;
hence A\B misses B by ENUMSET:def 12;
thus for X st X c= A & X misses B holds X c= A\B
proof
let X;
assume that xa: X c= A and xb: X misses B;
thus X c= A\B
proof
let x;
assume x: x in X;
then a: x in A by xa,ENUMSET:def 10;
X /\ B = {} by xb,ENUMSET:def 12;
then not x in X /\ B by ENUMSET:def 1;
then not x in B by x,ENUMSET:def 7;
hence x in A\B by a,ENUMSET:def 8;
end;
end;
end;
A\/B = union {A,B}
proof
thus A\/B c= union {A,B}
proof
let x;
assume x in A\/B;
then x in A or x in B by ENUMSET:def 6;
then x in A & A in {A,B} or x in B & B in {A,B} by ENUMSET:def 4;
hence x in union {A,B} by ENUMSET:def 13;
end;
thus union {A,B} c= A\/B
proof
let x;
assume x in union {A,B};
then consider Y being set such that
y: x in Y & Y in {A,B} by ENUMSET:def 13;
Y = A or Y = B by ENUMSET:def 4,y;
hence x in A\/B by y,ENUMSET:def 6;
end;
end;
A/\B = meet {A,B}
proof
a: A in {A,B} & B in {A,B} by ENUMSET:def 4;
then np: {A,B} <> {} by ENUMSET:def 1;
thus A/\B c= meet {A,B}
proof
let x;
assume x in A/\B;
then ab: x in A & x in B by ENUMSET:def 7;
for Y st Y in {A,B} holds x in Y
proof
let Y;
assume Y in {A,B};
then Y = A or Y = B by ENUMSET:def 4;
hence x in Y by ab;
end;
hence x in meet {A,B} by ENUMSET:def 14,np;
end;
thus meet {A,B} c= A/\B
proof
let x;
assume x in meet {A,B};
then x in A & x in B by a,ENUMSET:def 14,np;
hence x in A/\B by ENUMSET:def 7;
end;
end;
::6.28
for A st A <> {} holds
(for B st B in A holds meet A c= B) &
for X st (for B st B in A holds X c= B) holds X c= meet A
proof
let A;
assume np: A<>{};
thus for B st B in A holds meet A c= B
proof
let B;
assume b: B in A;
thus meet A c= B
proof
let x;
assume x in meet A;
hence x in B by b,np,ENUMSET:def 14;
end;
end;
let X;
assume X: for B st B in A holds X c= B;
thus X c= meet A
proof
let x;
assume x: x in X;
for Y st Y in A holds x in Y
proof
let Y;
assume Y in A;
then X c= Y by X;
hence x in Y by x,ENUMSET:def 10;
end;
hence x in meet A by np,ENUMSET:def 14;
end;
end;
::6.29
for A holds
(for B st B in A holds B c= union A) &
(for X st (for B st B in A holds B c= X) holds union A c= X)
proof
let A;
thus for B st B in A holds B c= union A
proof
let B;
assume b: B in A;
thus B c= union A
proof
let x;
assume x in B;
hence x in union A by b,ENUMSET:def 13;
end;
end;
let X;
assume b: for B st B in A holds B c= X;
thus union A c= X
proof
let x;
assume x in union A;
then consider Y such that
y: x in Y & Y in A by ENUMSET:def 13;
Y c= X by b,y;
hence x in X by y,ENUMSET:def 10;
end;
end;