environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,b,c,d,x,y,z,A,B,C for set;
lab:
{a,b} = {b,a}
proof
thus {a,b} c= {b,a}
proof
let x;
assume x in {a,b};
then x = a or x = b by ENUMSET:def 4;
hence x in {b,a} by ENUMSET:def 4;
end;
thus {b,a} c= {a,b}
proof
let x;
assume x in {b,a};
then x = b or x = a by ENUMSET:def 4;
hence x in {a,b} by ENUMSET:def 4;
end;
end;
laa:
{a,a} = {a}
proof
thus {a,a} c= {a}
proof
let x;
assume x in {a,a};
then x = a by ENUMSET:def 4;
hence x in {a} by ENUMSET:def 3;
end;
thus {a} c= {a,a}
proof
let x;
assume x in {a};
then x = a by ENUMSET:def 3;
hence x in {a,a} by ENUMSET:def 4;
end;
end;
{a,b} = {a} \/ {b}
proof
thus {a,b} c= {a} \/ {b}
proof
let x;
assume x in {a,b};
then x = a or x = b by ENUMSET:def 4;
then x in {a} or x in {b} by ENUMSET:def 3;
hence x in {a} \/ {b} by ENUMSET:def 6;
end;
thus {a} \/ {b} c= {a,b}
proof
let x;
assume x in {a} \/ {b};
then x in {a} or x in {b} by ENUMSET:def 6;
then x = a or x = b by ENUMSET:def 3;
hence x in {a,b} by ENUMSET:def 4;
end;
end;
{a,b} \/ {c} = {a} \/ {b,c}
proof
thus {a,b} \/ {c} c= {a} \/ {b,c}
proof
let x;
assume x in {a,b} \/ {c};
then x in {a,b} or x in {c} by ENUMSET:def 6;
then x = a or x = b or x = c by ENUMSET:def 4,def 3;
then x in {a} or x in {b,c} by ENUMSET:def 3,def 4;
hence x in {a} \/ {b,c} by ENUMSET:def 6;
end;
thus {a} \/ {b,c} c= {a,b} \/ {c}
proof
let x;
assume x in {a} \/ {b,c};
then x in {a} or x in {b,c} by ENUMSET:def 6;
then x = a or x = b or x = c by ENUMSET:def 3,def 4;
then x in {a,b} or x in {c} by ENUMSET:def 4,def 3;
hence x in {a,b} \/ {c} by ENUMSET:def 6;
end;
end;
labe:
{a} = {b} implies a=b
proof
assume {a}={b};
then b in {a} by ENUMSET:def 3;
hence a=b by 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,ac;
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 {c,d}={a};
then c in {a} & d in {a} by ENUMSET:def 4;
then cad: 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;
then contradiction by ab;
hence thesis;
end;
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};
then c in {a} by ENUMSET:def 3;
hence contradiction by arc,ENUMSET:def 3;
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 arb,bd,ENUMSET:def 4;
end;
end;
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};
then c in {a} by ENUMSET:def 3;
hence contradiction by arc,ENUMSET:def 3;
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 arb,bd,ENUMSET:def 4;
end;
end;
end;
end;
thus a = c & b = d implies [a, b] = [c, d];
end;