environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
::equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,x,y,z,A,B,C for set;
::2.119
Lm1:
for A,B holds A \+\ B = (A \/ B) \ (A /\ B)
proof
let A,B be set;
thus A \+\ B c= (A \/ B) \ (A /\ B)
proof
let x be set;
assume x in A \+\ B;
then x in (A \ B) \/ (B \ A) by ENUMSET:def 9;
then x in A \ B or x in B \ A by ENUMSET:def 6;
then (x in A & not x in B) or (x in B & not x in A) by ENUMSET:def 8;
:: then (x in A or x in B) & not (x in A & x in B);
then x in A \/ B & not x in A /\ B by ENUMSET:def 6,def 7;
:: thus then x in (A \/ B) \ (A /\ B) by ENUMSET:def 8;
hence x in (A \/ B) \ (A /\ B) by ENUMSET:def 8;
end;
thus (A \/ B) \ (A /\ B) c= A \+\ B
proof
let y be set;
assume y in (A \/ B) \ (A /\ B);
then y in A \/ B & not y in A /\ B by ENUMSET:def 8;
then (y in A or y in B) & not (y in A & y in B) by ENUMSET:def 6,def 7;
:: then (y in A & not y in B) or (y in B & not y in A);
then y in A \ B or y in B \ A by ENUMSET:def 8;
then y in (A \ B) \/ (B \ A) by ENUMSET:def 6;
hence y in A \+\ B by ENUMSET:def 9;
end;
end;
Lm0:
A \/ B = B \/ A
proof
thus A \/ B c= B \/ A
proof
let a be set;
assume a in A \/ B;
then a in A or a in B by ENUMSET:def 6;
:: then a in B or a in A;
hence a in B \/ A by ENUMSET:def 6;
end;
thus B \/ A c= A \/ B
proof
let a be set;
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
A \+\ B = (A \ B) \/ (B \ A) by ENUMSET:def 9
.= (B \ A) \/ (A \ B) by Lm0
.= B \+\ A by ENUMSET:def 9;
hence thesis;
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 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;