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