Theorem:
ALL(null):ALL(s):[Set(null)
& ALL(a):~a e null
& Set(s)
& ALL(a):[a e s <=> ~a=a]
=> null=s]
Proof
-----
Initial premise
1 Set(null)
& ALL(a):~a e null
& Set(s)
& ALL(a):[a e s <=> ~a=a]
Premise
Define: null
2 Set(null)
Split, 1
3 ALL(a):~a e null
Split, 1
Define: s
4 Set(s)
Split, 1
5 ALL(a):[a e s <=> ~a=a]
Split, 1
Prove: null = s
Apply set equality axiom for null and s.
6 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
7 ALL(b):[Set(null) & Set(b) => [null=b <=> ALL(c):[c e null <=> c e b]]]
U Spec, 6
8 Set(null) & Set(s) => [null=s <=> ALL(c):[c e null <=> c e s]]
U Spec, 7
9 Set(null) & Set(s)
Join, 2, 4
10 null=s <=> ALL(c):[c e null <=> c e s]
Detach, 8, 9
11 [null=s => ALL(c):[c e null <=> c e s]]
& [ALL(c):[c e null <=> c e s] => null=s]
Iff-And, 10
12 null=s => ALL(c):[c e null <=> c e s]
Split, 11
Sufficient: For null=s
13 ALL(c):[c e null <=> c e s] => null=s
Split, 11
Prove: ALL(a):[a e null => a e s]
Suppose...
14 x e null
Premise
Apply definition of null
15 ~x e null
U Spec, 3
Apply arbitrary consequent rule
16 ~~x e null => x e s
Arb Cons, 15
17 x e null => x e s
Rem DNeg, 16
18 x e s
Detach, 17, 14
As Required:
19 ALL(a):[a e null => a e s]
4 Conclusion, 14
Prove: ALL(a):[a e s => a e null]
Suppose...
20 x e s
Premise
Apply definition of s
21 x e s <=> ~x=x
U Spec, 5
22 [x e s => ~x=x] & [~x=x => x e s]
Iff-And, 21
23 x e s => ~x=x
Split, 22
24 ~x=x => x e s
Split, 22
25 ~x=x
Detach, 23, 20
Apply arbitrary consequent rule
26 ~~x=x => x e null
Arb Cons, 25
27 x=x => x e null
Rem DNeg, 26
Apply reflexivity axiom
28 x=x
Reflex
29 x e null
Detach, 27, 28
As Required:
30 ALL(a):[a e s => a e null]
4 Conclusion, 20
Joining results...
31 ALL(a):[[a e null => a e s] & [a e s => a e null]]
Join, 19, 30
32 ALL(a):[a e null <=> a e s]
Iff-And, 31
As Required:
33 null=s
Detach, 13, 32
As Required:
34 ALL(null):ALL(s):[Set(null)
& ALL(a):~a e null
& Set(s)
& ALL(a):[a e s <=> ~a=a]
=> null=s]
4 Conclusion, 1