THEOREM
*******
ALL(e):ALL(e'):[Set(e)
& Set(e')
=> [ALL(a):~a e e & ALL(a):~a e
e' => e=e']]
By Dan Christensen
PROOF
*****
Let e and e' be sets
1 Set(e) & Set(e')
Premise
2 Set(e)
Split, 1
3 Set(e')
Split, 1
Prove: ALL(a):~a e e & ALL(a):~a e
e' => e=e'
Suppose e and e’
are empty
4 ALL(a):~a e e & ALL(a):~a e e'
Premise
5 ALL(a):~a e e
Split, 4
6 ALL(a):~a e e'
Split, 4
Apply Set Equality
Axiom
7 ALL(a):ALL(b):[Set(a) &
Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set
Equality
8 ALL(b):[Set(e) & Set(b) => [e=b <=> ALL(c):[c e e <=> c e b]]]
U Spec, 7
9 Set(e) & Set(e') => [e=e' <=> ALL(c):[c e e <=> c e e']]
U Spec, 8
10 e=e' <=> ALL(c):[c e e <=> c e e']
Detach, 9,
1
11 [e=e' => ALL(c):[c e e <=> c e e']]
& [ALL(c):[c e e <=> c e e'] => e=e']
Iff-And, 10
12 e=e' => ALL(c):[c e e <=> c e e']
Split, 11
Sufficient: For
e=e'
13 ALL(c):[c e e <=> c e e'] => e=e'
Split, 11
'=>'
Prove:
ALL(c):[c e e => c e e']
Suppose...
14 x e e
Premise
15 ~x e e
U Spec, 5
Vacuously
true:
16 ~x e e => x e e'
Arb Cons, 14
17 x e e'
Detach, 16, 15
As Required:
18 ALL(c):[c e e => c e e']
4 Conclusion,
14
'<='
Prove:
ALL(c):[c e e' => c e e]
Suppose...
19 x e e'
Premise
20 ~x e e'
U Spec, 6
Vacuously
true:
21 ~x e e' => x e e
Arb Cons, 19
22 x e e
Detach, 21, 20
As Required:
23 ALL(c):[c e e' => c e e]
4 Conclusion,
19
Joining results...
24 ALL(c):[[c e e => c e e'] & [c e e' => c e e]]
Join, 18,
23
25 ALL(c):[c e e <=> c e e']
Iff-And, 24
26 e=e'
Detach, 13,
25
As Required:
27 ALL(a):~a e e & ALL(a):~a e e' => e=e'
4 Conclusion,
4
As Required:
28 ALL(e):ALL(e'):[Set(e)
& Set(e')
=> [ALL(a):~a e e
& ALL(a):~a e e' => e=e']]
4 Conclusion,
1