THEOREM
*******
ALL(s):[Set(s)
=> EXIST(null):EXIST(f):[Set(null) & Set'(f)
& [ALL(a):~a
e null & ALL(a):ALL(b):~(a,b) e f
& ALL(a):[a
e null => f(a) e s]]]]
The proof could be shortened
considerably since anything whatsoever would follow from the presumed existence
of any element of an empty set. Here, however, we actually construct the
function f using the axioms of set theory.
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
PROOF
*****
Suppose...
2 Set(s)
Premise
Construct empty subset of s
Apply Subset Axiom
3 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]
Subset, 2
4 Set(null) & ALL(a):[a e null <=> a e s & ~a e s]
E Spec, 3
Define: null
(empty subset of s)
5 Set(null)
Split, 4
6 ALL(a):[a e null <=> a e s & ~a e s]
Split, 4
Prove: ~EXIST(a):a e null
Suppose to the contrary...
7 x e null
Premise
Apply definition of null
8 x e null <=> x e s & ~x e s
U Spec, 6
9 [x e null => x e s & ~x e s]
&
[x e s & ~x e s => x e null]
Iff-And, 8
10 x e null => x e s & ~x e s
Split, 9
11 x e s & ~x e s => x e null
Split, 9
12 x e s & ~x e s
Detach, 10, 7
As Required:
13 ~EXIST(a):a e null
4 Conclusion, 7
Change quantifier
14 ~~ALL(a):~a e null
Quant, 13
As Required:
15 ALL(a):~a e null
Rem DNeg, 14
Construct Cartesian product of null and s
Apply Cartesian Product Axiom
16 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
17 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, 16
18 Set(null) & Set(s) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e s]]
U Spec, 17
19 Set(null) & Set(s)
Join, 5, 2
20 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e s]]
Detach, 18, 19
21 Set'(nullxs) & ALL(c1):ALL(c2):[(c1,c2) e nullxs <=> c1 e null & c2 e s]
E Spec, 20
Define: nullxs (Cartesian product
of null and s)
22 Set'(nullxs)
Split, 21
23 ALL(c1):ALL(c2):[(c1,c2) e nullxs <=> c1 e null & c2 e s]
Split, 21
Prove: ~EXIST(a):EXIST(b):(a,b) e nullxs
Suppose to the contrary...
24 (x,y) e nullxs
Premise
Apply definition of nullxs
25 ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]
U Spec, 23
26 (x,y) e nullxs <=> x e null & y e s
U Spec, 25
27 [(x,y) e nullxs => x e null & y e s]
&
[x e null & y e s => (x,y) e nullxs]
Iff-And, 26
28 (x,y) e nullxs => x e null & y e s
Split, 27
29 x e null & y e s => (x,y) e nullxs
Split, 27
30 x e null & y e s
Detach, 28, 24
31 x e null
Split, 30
32 y e s
Split, 30
Apply definition of null
33 ~x e null
U Spec, 15
Obtain the contradiction...
34 x e null & ~x e null
Join, 31, 33
As Required:
35 ~EXIST(a):EXIST(b):(a,b) e nullxs
4 Conclusion, 24
Change quantifiers
36 ~~ALL(a):~EXIST(b):(a,b) e nullxs
Quant, 35
37 ALL(a):~EXIST(b):(a,b) e nullxs
Rem DNeg, 36
38 ALL(a):~~ALL(b):~(a,b) e nullxs
Quant, 37
As Required:
39 ALL(a):ALL(b):~(a,b) e nullxs
Rem DNeg, 38
Apply Axiom of Functionality
40 ALL(a):ALL(b):[Set'(nullxs) & Set(a) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e nullxs => c e a & d e b]
&
ALL(c):[c e a =>
EXIST(d):[d e b & (c,d) e nullxs]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
=>
ALL(c):ALL(d):[c e a & d e b => [d=nullxs(c) <=> (c,d) e nullxs]]]]
U Spec, 1
41 ALL(b):[Set'(nullxs) & Set(null) & Set(b)
=>
[ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e b]
&
ALL(c):[c e null =>
EXIST(d):[d e b & (c,d) e nullxs]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e b => [d=nullxs(c) <=> (c,d) e nullxs]]]]
U Spec, 40
42 Set'(nullxs) & Set(null) & Set(s)
=>
[ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]
&
ALL(c):[c e null =>
EXIST(d):[d e s & (c,d) e nullxs]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e s => [d=nullxs(c) <=> (c,d) e nullxs]]]
U Spec, 41
43 Set'(nullxs) & Set(null)
Join, 22, 5
44 Set'(nullxs) & Set(null) & Set(s)
Join, 43, 2
Sufficient: For functionality of nullxs
45 ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]
&
ALL(c):[c e null =>
EXIST(d):[d e s & (c,d) e nullxs]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
=>
ALL(c):ALL(d):[c e null & d e s => [d=nullxs(c) <=> (c,d) e nullxs]]
Detach, 42, 44
Part 1
Prove: ALL(c):ALL(d):[(c,d) e nullxs
=> c e null & d e s]
Suppose...
46 (x,y) e nullxs
Premise
Apply definition of nullxs
47 ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]
U Spec, 23
48 (x,y) e nullxs <=> x e null & y e s
U Spec, 47
49 [(x,y) e nullxs => x e null & y e s]
&
[x e null & y e s => (x,y) e nullxs]
Iff-And, 48
50 (x,y) e nullxs => x e null & y e s
Split, 49
51 x e null & y e s => (x,y) e nullxs
Split, 49
52 x e null & y e s
Detach, 50, 46
Part 1
As Required:
53 ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]
4 Conclusion, 46
Part 2
Prove: ALL(c):[c e null => EXIST(d):[d e s & (c,d) e nullxs]]
Suppose...
54 x e null
Premise
Apply definition of null
55 ~x e null
U Spec, 15
Apply principle of explosion
56 ~x e null => EXIST(d):[d e s & (x,d) e nullxs]
Arb Cons, 54
57 EXIST(d):[d e s & (x,d) e nullxs]
Detach, 56, 55
Part 2
As Required:
58 ALL(c):[c e null =>
EXIST(d):[d e s & (c,d) e nullxs]]
4 Conclusion, 54
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1)
e nullxs & (c,d2) e nullxs => d1=d2]
Suppose...
59 (x,y1) e nullxs & (x,y2) e nullxs
Premise
60 (x,y1) e nullxs
Split, 59
61 (x,y2) e nullxs
Split, 59
Apply definition of nullxs
62 ALL(c2):[(x,c2) e nullxs <=> x e null & c2 e s]
U Spec, 23
63 (x,y1) e nullxs <=> x e null & y1 e s
U Spec, 62
64 [(x,y1) e nullxs => x e null & y1 e s]
&
[x e null & y1 e s => (x,y1) e nullxs]
Iff-And, 63
65 (x,y1) e nullxs => x e null & y1 e s
Split, 64
66 x e null & y1 e s => (x,y1) e nullxs
Split, 64
67 x e null & y1 e s
Detach, 65, 60
68 x e null
Split, 67
69 y1 e s
Split, 67
Apply definition of null
70 ~x e null
U Spec, 15
Apply principle of explosion
71 ~x e null => y1=y2
Arb Cons, 68
72 y1=y2
Detach, 71, 70
Part 3
As Required:
73 ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
4 Conclusion, 59
Joining results...
74 ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]
&
ALL(c):[c e null =>
EXIST(d):[d e s & (c,d) e nullxs]]
Join, 53, 58
75 ALL(c):ALL(d):[(c,d) e nullxs => c e null & d e s]
&
ALL(c):[c e null =>
EXIST(d):[d e s & (c,d) e nullxs]]
&
ALL(c):ALL(d1):ALL(d2):[(c,d1) e nullxs & (c,d2) e nullxs => d1=d2]
Join, 74, 73
As Required:
nullxs is function
76 ALL(c):ALL(d):[c e null & d e s => [d=nullxs(c) <=> (c,d) e nullxs]]
Detach, 45, 75
Prove: ALL(a):[a e null => nullxs(a) e s]
Suppose...
77 x e null
Premise
Apply Part 2
78 x e null => EXIST(d):[d e s & (x,d) e nullxs]
U Spec, 58
79 EXIST(d):[d e s & (x,d) e nullxs]
Detach, 78, 77
80 y e s & (x,y) e nullxs
E Spec, 79
81 y e s
Split, 80
82 (x,y) e nullxs
Split, 80
Apply functionality of nullxs
83 ALL(d):[x e null & d e s => [d=nullxs(x) <=> (x,d) e nullxs]]
U Spec, 76
84 x e null & y e s => [y=nullxs(x) <=> (x,y) e nullxs]
U Spec, 83
85 x e null & y e s
Join, 77, 81
86 y=nullxs(x) <=> (x,y) e nullxs
Detach, 84, 85
87 [y=nullxs(x) => (x,y) e nullxs]
&
[(x,y) e nullxs => y=nullxs(x)]
Iff-And, 86
88 y=nullxs(x) => (x,y) e nullxs
Split, 87
89 (x,y) e nullxs => y=nullxs(x)
Split, 87
90 y=nullxs(x)
Detach, 89, 82
91 nullxs(x) e s
Substitute, 90,
81
As Required:
92 ALL(a):[a e null => nullxs(a) e s]
4 Conclusion, 77
Joining results...
93 Set(null) & Set'(nullxs)
Join, 5, 22
94 ALL(a):~a e null &
ALL(a):ALL(b):~(a,b) e nullxs
Join, 15, 39
95 ALL(a):~a e null &
ALL(a):ALL(b):~(a,b) e nullxs
&
ALL(a):[a e null => nullxs(a) e s]
Join, 94, 92
96 Set(null) & Set'(nullxs)
&
[ALL(a):~a e null &
ALL(a):ALL(b):~(a,b) e nullxs
&
ALL(a):[a e null => nullxs(a) e s]]
Join, 93, 95
As Required:
97 ALL(s):[Set(s)
=>
EXIST(null):EXIST(f):[Set(null) & Set'(f)
&
[ALL(a):~a e null & ALL(a):ALL(b):~(a,b) e f
&
ALL(a):[a e null => f(a) e s]]]]
4 Conclusion, 2