environ
vocabularies ENUMSET;
notations ENUMSET;
constructors ENUMSET;
definitions ENUMSET;
equalities ENUMSET;
theorems ENUMSET;
begin
reserve a,b,c,d,x,x1,x2,y1,y2,y,z,A,B,C,X,Y 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] = [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;
[a,b] = {{a}, {a, b}} by ENUMSET:def 5,lab;
then [a,b] = {{a}, {a, a}} by ab;
then [a,b] = {{a}, {a}} by laa;
then [a,b] = {{a}} by laa;
then [c,d] = {{a}} by abc;
then {{c,d},{c}} = {{a}} by ENUMSET:def 5;
then c: {{c},{c,d}} = {{a}} by lab;
{c} in {{c},{c,d}} & {c,d} in {{c},{c,d}} by ENUMSET:def 4;
then {c} in {{a}} & {c,d} in {{a}} by c;
then {c} = {a} & {c,d} = {a} by ENUMSET:def 3;
then c in {a} & d in {a} by ENUMSET:def 4;
then c = a & d=a by ENUMSET:def 3;
hence a=c & 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 {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;
end;
end;
thus a = c & b = d implies [a, b] = [c, d];
end;