THEOREM
*******
EXIST(f):[Set'(f)
& ALL(a):ALL(b):~(a,b) e f & ALL(a):[a e null =>
f(a) e null]]
where null is a set such that
ALL(a):~a e null
This machine-verified formal
proof was written with the aid of the author's DC Proof 2.0 software available
at http://www.dcproof.com
AXIOMS
******
Axiom of functionality for 1
variable
1 ALL(f):ALL(a):ALL(b):[Set'(f) &
Set(a) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e f => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e f]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=f(c) <=> (c,d) e f]]]]
Axiom
Define: The null set
2 Set(null)
Axiom
3 ALL(a):~a e null
Axiom
PROOF
*****
Construct the Cartesian product
null x null
Apply the Cartesian Product
Axiom
4 ALL(a1):ALL(a2):[Set(a1) & Set(a2) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
5 ALL(a2):[Set(null) & Set(a2) => EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e a2]]]
U Spec, 4
6 Set(null) & Set(null) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e null]]
U Spec, 5
7 Set(null) & Set(null)
Join, 2, 2
8 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e null]]
Detach, 6, 7
9 Set'(null2) & ALL(c1):ALL(c2):[(c1,c2) e null2 <=> c1 e null & c2 e null]
E Spec, 8
Define: null2 (null x null)
10 Set'(null2)
Split, 9
11 ALL(c1):ALL(c2):[(c1,c2) e null2 <=> c1 e null & c2 e null]
Split, 9
As Required:
23 ~EXIST(a):EXIST(b):(a,b) e null2
5 Conclusion, 12
Prove: ALL(a):ALL(b):~(a,b) e null2
Apply Quantifier Switch and
Remove Double Negation Axioms
24 ~~ALL(a):~EXIST(b):(a,b) e null2
Quant, 23
25 ALL(a):~EXIST(b):(a,b) e null2
Rem DNeg, 24
26 ALL(a):~~ALL(b):~(a,b) e null2
Quant, 25
As Required:
null2 is a set of ordered pairs
that is empty
27 ALL(a):ALL(b):~(a,b) e null2
Rem DNeg, 26
Apply functionality axiom
28 ALL(a):ALL(b):[Set'(null2) & Set(a) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e null2 => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e null2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=null2(c) <=> (c,d) e null2]]]]
U Spec, 1
29 ALL(b):[Set'(null2) & Set(null) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e null2 => c e null & d e b]
&
ALL(c):[c e null =>
EXIST(d):[d e b & (c,d) e null2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e b => [d=null2(c) <=> (c,d) e null2]]]]
U Spec, 28
30 Set'(null2) & Set(null) & Set(null)
=>
[ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]
&
ALL(c):[c e null =>
EXIST(d):[d e null & (c,d) e null2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]]
U Spec, 29
31 Set'(null2) & Set(null)
Join, 10, 2
32 Set'(null2) & Set(null) & Set(null)
Join, 31, 2
Sufficient: For functionality
of null2
33 ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]
&
ALL(c):[c e null =>
EXIST(d):[d e null & (c,d) e null2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]
Detach, 30, 32
Part 1
As Required:
39 ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]
5 Conclusion, 34
Part 2
As Required:
44 ALL(c):[c e null =>
EXIST(d):[d e null & (c,d) e null2]]
5 Conclusion, 40
Part 3
As Required:
52 ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
5 Conclusion, 45
53 ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]
&
ALL(c):[c e null =>
EXIST(d):[d e null & (c,d) e null2]]
Join, 39, 44
54 ALL(c):ALL(d):[(c,d) e null2 => c e null & d e null]
&
ALL(c):[c e null =>
EXIST(d):[d e null & (c,d) e null2]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e null2 & (c,d2) e null2 => d1=d2]
Join, 53, 52
null2 is a function mapping the
null set to itself
55 ALL(c):ALL(d):[c e null & d e null => [d=null2(c) <=> (c,d) e null2]]
Detach, 33, 54
As Required:
71 ALL(a):[a e null => null2(a) e null]
5 Conclusion, 56
Joining previous results...
72 Set'(null2) & ALL(a):ALL(b):~(a,b) e null2
Join, 10, 27
73 Set'(null2) & ALL(a):ALL(b):~(a,b) e null2
&
ALL(a):[a e null => null2(a) e null]
Join, 72, 71
Generalizing...
As Required:
74 EXIST(f):[Set'(f) & ALL(a):ALL(b):~(a,b) e f
&
ALL(a):[a e null => f(a) e null]]
E Gen, 73