environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
theorems ENUMSET;
begin
reserve A,B,C,X,Y,Z,a,b,c,x,y,z for set;
Lm0:
A \/ B = B \/ A
proof
thus A \/ B c= B \/ A
proof
let a;
assume a in A\/B;
then a in A or a in B by ENUMSET:def 6;
hence a in B\/A by ENUMSET:def 6;
end;
thus B \/ A c= A \/ B
proof
let a;
assume a in B\/A;
then a in B or a in A by ENUMSET:def 6;
hence a in A\/B by ENUMSET:def 6;
end;
end;
::2.114
A \+\ B = B \+\ A
proof
thus A \+\ B c= B \+\ A
proof
let a;
assume a in A \+\ B;
then a in (A \ B) \/ (B \ A) by ENUMSET:def 9;
then a in (A \ B) or a in (B \ A) by ENUMSET:def 6;
:: then a in (B \ A) or a in (A \ B);
then a in (B \ A) \/ (A \ B) by ENUMSET:def 6;
hence a in B \+\ A by ENUMSET:def 9;
end;
thus B \+\ A c= A \+\ B
proof
let a;
assume a in B \+\ A;
then a in (B \ A) \/ (A \ B) by ENUMSET:def 9;
then a in (B \ A) or a in (A \ B) by ENUMSET:def 6;
then a in (A \ B) \/ (B \ A) by ENUMSET:def 6;
hence a in A \+\ B by ENUMSET:def 9;
end;
end;
A \+\ B = B \+\ A
proof
A \+\ B = (A\B) \/ (B\A) by ENUMSET:def 9;
then A \+\ B = (B\A) \/ (A\B) by Lm0;
hence A \+\ B = B \+\ A by ENUMSET:def 9;
end;
::2.119
Lm1:
A \+\ B = (A\/B) \ (A/\B)
proof
thus A \+\ B c= (A\/B) \ (A/\B)
proof
let a;
assume a in A \+\ B;
then a in (A\B) \/ (B\A) by ENUMSET:def 9;
then a in A\B or a in B\A by ENUMSET:def 6;
then per cases;
suppose a in A\B;
then a in A & not a in B by ENUMSET:def 8;
then a in A\/B & not a in A/\B by ENUMSET:def 6,def 7;
hence a in (A\/B) \ (A/\B) by ENUMSET:def 8;
end;
suppose a in B\A;
then a in B & not a in A by ENUMSET:def 8;
then a in A\/B & not a in A/\B by ENUMSET:def 6,def 7;
hence a in (A\/B) \ (A/\B) by ENUMSET:def 8;
end;
end;
thus (A\/B) \ (A/\B) c= A \+\ B
proof
let a;
assume a in (A\/B) \ (A/\B);
then a in A\/B & not a in A/\B by ENUMSET:def 8;
then (a in A or a in B) & (not a in A or not a in B) by ENUMSET:def 6,def 7;
:: then (a in A & not a in B) or (a in B & not a in A);
then a in A\B or a in B\A by ENUMSET:def 8;
then a in (A\B) \/ (B\A) by ENUMSET:def 6;
hence a in A \+\ B by ENUMSET:def 9;
end;
end;
::2.120
A\/B = (A \+\ B) \+\ (A/\B)
proof
thus A\/B c= (A \+\ B) \+\ (A/\B)
proof
let a;
assume a in A\/B;
then a in A or a in B by ENUMSET:def 6;
then per cases;
suppose aa: a in A;
per cases;
suppose a in B;
then ab: a in A/\B by aa,ENUMSET:def 7;
then not a in (A\/B) \ (A/\B) by ENUMSET:def 8;
then not a in (A \+\ B) by Lm1;
then a in (A/\B) \ (A \+\ B) by ab,ENUMSET:def 8;
:: then a in (A \+\ B) \ (A/\B) or a in (A/\B) \ (A \+\ B);
then a in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence a in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
suppose na: not a in B;
then ab: not a in A/\B by aa,ENUMSET:def 7;
a in A\B by aa,na,ENUMSET:def 8;
then a in (A\B) \/ (B\A) by ENUMSET:def 6;
then a in A \+\ B by ENUMSET:def 9;
then a in (A \+\ B) \ (A/\B) by ab,ENUMSET:def 8;
then a in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence a in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
end;
suppose aa: a in B;
per cases;
suppose a in A;
then ab: a in A/\B by aa,ENUMSET:def 7;
then not a in (A\/B) \ (A/\B) by ENUMSET:def 8;
then not a in (A \+\ B) by Lm1;
then a in (A/\B) \ (A \+\ B) by ab,ENUMSET:def 8;
then a in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence a in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
suppose na: not a in A;
then ab: not a in A/\B by aa,ENUMSET:def 7;
a in B\A by aa,na,ENUMSET:def 8;
then a in (A\B) \/ (B\A) by ENUMSET:def 6;
then a in A \+\ B by ENUMSET:def 9;
then a in (A \+\ B) \ (A/\B) by ab,ENUMSET:def 8;
then a in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 6;
hence a in (A \+\ B) \+\ (A/\B) by ENUMSET:def 9;
end;
end;
end;
thus (A \+\ B) \+\ (A/\B) c= A\/B
proof
let a;
assume a in (A \+\ B) \+\ (A/\B);
then a in ((A \+\ B) \ (A/\B)) \/ ((A/\B) \ (A \+\ B)) by ENUMSET:def 9;
then a in (A \+\ B) \ (A/\B) or a in (A/\B) \ (A \+\ B) by ENUMSET:def 6;
then per cases;
suppose a in (A \+\ B) \ (A/\B);
then a in (A \+\ B) & not a in A/\B by ENUMSET:def 8;
then a in (A\/B) \ (A/\B) by Lm1;
hence a in A \/ B by ENUMSET:def 8;
end;
suppose a in (A/\B) \ (A \+\ B);
then a in A/\B & not a in A \+\ B by ENUMSET:def 8;
then a in A & a in B by ENUMSET:def 7;
hence a in A \/ B by ENUMSET:def 6;
end;
end;
end;
::2.121
ex A,B,C st not A \/ (B\+\C) = (A\/B \+\ (A\/C))
proof
take A={1};
take B={};
take C={1};
s: 1 in A & 1 in C by ENUMSET:def 3;
then j: 1 in A \/ (B \+\ C) by ENUMSET:def 6;
not 1 in (A \/ B) \+\ (A \/ C)
proof
assume 1 in (A \/ B) \+\ (A \/ C);
then 1 in ((A \/ B) \/ (A \/ C)) \ ((A \/ B) /\ (A \/ C)) by Lm1;
then spr: 1 in (A \/ B) \/ (A \/ C) & not 1 in (A \/ B) /\ (A \/ C) by ENUMSET:def 8;
1 in A \/ B & 1 in A \/ C by s,ENUMSET:def 6;
then 1 in (A \/ B) /\ (A \/ C) by ENUMSET:def 7;
hence contradiction by spr;
end;
hence thesis by j;
end;