environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,b,c,d,e,x,y,z,A,B,C for set;
laa:
{x,x} = {x}
proof
thus {x,x} c= {x}
proof
let y;
assume y in {x,x};
then y = x or y = x by ENUMSET:def 4;
hence y in {x} by ENUMSET:def 3;
end;
thus {x} c= {x,x}
proof
let y;
assume y in {x};
then y = x by ENUMSET:def 3;
hence y in {x,x} by ENUMSET:def 4;
end;
end;
{x,y} = {y,x}
proof
thus {x,y} c= {y,x}
proof
let z;
assume z in {x,y};
then z = x or z = y by ENUMSET:def 4;
hence z in {y,x} by ENUMSET:def 4;
end;
thus {y,x} c= {x,y}
proof
let z;
assume z in {y,x};
then z = y or z = x by ENUMSET:def 4;
hence z in {x,y} by ENUMSET:def 4;
end;
end;
{x,y} = {x} \/ {y}
proof
thus {x,y} c= {x} \/ {y}
proof
let z;
assume z in {x,y};
then z = x or z = y by ENUMSET:def 4;
then z in {x} or z in {y} by ENUMSET:def 3;
hence z in {x} \/ {y} by ENUMSET:def 6;
end;
thus {x} \/ {y} c= {x,y}
proof
let z;
assume z in {x} \/ {y};
then z in {x} or z in {y} by ENUMSET:def 6;
then z = x or z = y by ENUMSET:def 3;
hence z in {x,y} by ENUMSET:def 4;
end;
end;
{x,y} \/ {z} = {x} \/ {y,z}
proof
thus {x,y} \/ {z} c= {x} \/ {y,z}
proof
let a;
assume a in {x,y} \/ {z};
then a in {x,y} or a in {z} by ENUMSET:def 6;
then a = x or a = y or a = z by ENUMSET:def 3,def 4;
then a in {x} or a in {y,z} by ENUMSET:def 3,def 4;
hence a in {x} \/ {y,z} by ENUMSET:def 6;
end;
thus {x} \/ {y,z} c= {x,y} \/ {z}
proof
let a;
assume a in {x} \/ {y,z};
then a in {x} or a in {y,z} by ENUMSET:def 6;
then a = x or a = y or a = z by ENUMSET:def 3,def 4;
then a in {x,y} or a in {z} by ENUMSET:def 3,def 4;
hence a in {x,y} \/ {z} by ENUMSET:def 6;
end;
end;
labe:
{x} = {y} implies x = y
proof
assume a: {x} = {y};
assume not x = y;
then not y in {x} by ENUMSET:def 3;
hence contradiction by a,ENUMSET:def 3;
end;
[a,b] = [c,d] iff a = c & b = d
proof
thus [a,b] = [c,d] implies a = c & b = d
proof
assume abc: [a,b] = [c,d];
per cases;
suppose ab: a=b;
then
[a,b] = {{a,a},{a}};
then [a,b] = {{a},{a}} by laa;
then [a,b] = {{a}} by laa;
then cda: [c,d] = {{a}} by abc;
then {c} in {{a}} by ENUMSET:def 4;
then {c} = {a} by ENUMSET:def 3;
hence ac: a = c by labe;
{c,d} in {{a}} by cda,ENUMSET:def 4;
then {c,d} = {a} by ENUMSET:def 3;
then d in {a} by ENUMSET:def 4;
then d = a by ENUMSET:def 3;
hence b = d by ab;
end;
suppose ab: a<>b;
s: {{a,b},{a}} = {{c,d},{c}} by abc;
then {c,d} in {{a,b},{a}} by ENUMSET:def 4;
then per cases by ENUMSET:def 4;
suppose cdab: {c,d} = {a,b};
thus ac: a = c
proof
assume arc: a <> c;
{a} in {{c,d},{c}} by s,ENUMSET:def 4;
then per cases by ENUMSET:def 4;
suppose {a} = {c,d};
then c in {a} by ENUMSET:def 4;
hence contradiction by arc,ENUMSET:def 3;
end;
suppose {a} = {c};
hence contradiction by arc,labe;
end;
end;
thus b = d
proof
assume bd: b<>d;
b in {c,d} by cdab,ENUMSET:def 4;
then b = c by bd,ENUMSET:def 4;
then arb: a=b by ac;
d in {a,b} by cdab,ENUMSET:def 4;
hence contradiction by ENUMSET:def 4,bd,arb;
end;
end;
suppose {c,d} = {a};
then c in {a} & d in {a} by ENUMSET:def 4;
then c = a & d = a by ENUMSET:def 3;
then {{a,b},{a}} = {{a,a},{a}} by s;
then {{a,b},{a}} = {{a},{a}} by laa;
then {{a,b},{a}} = {{a}} by laa;
then {a,b} in {{a}} by ENUMSET:def 4;
then {a,b} = {a} by ENUMSET:def 3;
then b in {a} by ENUMSET:def 4;
then b = a by ENUMSET:def 3;
hence a = c & b = d by ab;
end;
end;
end;
thus a = c & b = d implies [a,b] = [c,d];
end;