THEOREM
*******
1. On every set, there is
exists a unique empty function (lines 1-91)
ALL(x):[Set(x)
=> EXIST(f):[ALL(a):[a
e null => f(a) e x]
& ALL(g):[ALL(a):[a
e null => g(a) e x] =>
g=f]]]
2. The function space (fs) of all
functions mapping the empty set to any set x has only a single element (lines
92-137)
ALL(x):[Set(x)
=> EXIST(fs):EXIST(f1):[Set(fs)
& f1 e fs
& [ALL(f):[f e fs <=> ALL(a):[a e null =>
f(a) e x]] <--- Function
space fs
& ALL(f2):[f2
e fs => f2=f1]]]]
HIGHLIGHTS
**********
Function Axiom cited on line 27.
Existence of function f established
in terms of graph set nx on line 54.
Function Equality Axiom cited
on lines 72, 115.
Function Space Axiom cited on
line 93.
Vacuous truth (Arb Cons Axiom) cited
on lines 37, 42, 46, 84, 127.
By Dan Christensen
2022-03-28
Homepage: http://www.dcproof.com
PROOF
*****
Define: Equality of functions
(1 variable)
Only functions with the same
domain and codomain are comparable here.
1 ALL(dom):ALL(cod):ALL(f):ALL(g):[Set(dom) & Set(cod) & ALL(a):[a e dom => f(a) e cod] & ALL(a):[a e dom => g(a) e cod]
=>
[f=g <=> ALL(a):[a e dom => f(a)=g(a)]]]
Axiom
Define: null (The empty set)
2 Set(null)
Axiom
3 ALL(a):~a e null
Axiom
Let x be an arbitrary set
4 Set(x)
Premise
Apply the Cartesian Producut Axiom
5 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
6 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, 5
7 Set(null) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
U Spec, 6
8 Set(null) & Set(x)
Join, 2, 4
9 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e null & c2 e x]]
Detach, 7, 8
10 Set'(nx) & ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]
E Spec, 9
Define: nx (The Cartesian
product of null and x, graph set of required function f)
11 Set'(nx)
Split, 10
12 ALL(c1):ALL(c2):[(c1,c2) e nx <=> c1 e null & c2 e x]
Split, 10
Prove: nx is an empty set of
ordered pairs
Suppose to the contrary...
13 (t,u) e nx
Premise
Apply the definition of nx
14 ALL(c2):[(t,c2) e nx <=> t e null & c2 e x]
U Spec, 12
15 (t,u) e nx <=> t e null & u e x
U Spec, 14
16 [(t,u) e nx => t e null & u e x]
&
[t e null & u e x => (t,u) e nx]
Iff-And, 15
17 (t,u) e nx => t e null & u e x
Split, 16
18 t e null & u e x
Detach, 17, 13
19 t e null
Split, 18
20 ~t e null
U Spec, 3
21 t e null & ~t e null
Join, 19, 20
As Required:
22 ~EXIST(a):EXIST(b):(a,b) e nx
4 Conclusion, 13
23 ~~ALL(a):~EXIST(b):(a,b) e nx
Quant, 22
24 ALL(a):~EXIST(b):(a,b) e nx
Rem DNeg, 23
25 ALL(a):~~ALL(b):~(a,b) e nx
Quant, 24
nx is an empty
set of ordered pairs
26 ALL(a):ALL(b):~(a,b) e nx
Rem DNeg, 25
Prove: nx is the graph of an empty
function
Apply Function Axiom (1 variable)
27 ALL(dom):ALL(cod):ALL(gra):[Set(dom) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e dom & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
Function
28 ALL(cod):ALL(gra):[Set(null) & Set(cod)
& Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e cod]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e cod & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e cod & b2 e cod
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e cod
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 27
29 ALL(gra):[Set(null) & Set(x) & Set'(gra)
=>
[ALL(a1):ALL(b):[(a1,b) e gra => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e gra]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e gra & (a1,b2) e gra => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e gra]]]]
U Spec, 28
30 Set(null) & Set(x) & Set'(nx)
=>
[ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]]
U Spec, 29
31 Set(null) & Set(x)
Join, 2, 4
32 Set(null) & Set(x) & Set'(nx)
Join, 31, 11
Sufficient: For functionality of nx
(Each precondition is vacuously true)
33 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
=>
EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]
Detach, 30, 32
Part 1
Prove: ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
Suppose...
34 (t,u) e nx
Premise
35 ALL(b):~(t,b) e nx
U Spec, 26
36 ~(t,u) e nx
U Spec, 35
37 ~(t,u) e nx => t e null & u e x
Arb Cons, 34
38 t e null & u e x
Detach, 37, 36
Part 1
As Required:
39 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
4 Conclusion, 34
Part 2
Prove: ALL(a1):[a1 e null => EXIST(b):[b e x &
(a1,b) e nx]]
Suppose...
40 t e null
Premise
41 ~t e null
U Spec, 3
42 ~t e null => EXIST(b):[b e x & (t,b) e nx]
Arb Cons, 40
43 EXIST(b):[b e x & (t,b) e nx]
Detach, 42, 41
Part 2
As Required:
44 ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
4 Conclusion, 40
Part 3
Prove: ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=> [(a1,b1) e nx &
(a1,b2) e nx => b1=b2]]
Suppose...
45 t e null & u1 e x & u2 e x
Premise
46 t e null
Split, 45
47 ~t e null
U Spec, 3
48 ~t e null => [(t,u1) e nx & (t,u2) e nx => u1=u2]
Arb Cons, 46
49 (t,u1) e nx & (t,u2) e nx => u1=u2
Detach, 48, 47
Part 3
As Required:
50 ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
4 Conclusion, 45
Joining results...
51 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
Join, 39, 44
52 ALL(a1):ALL(b):[(a1,b) e nx => a1 e null & b e x]
&
ALL(a1):[a1 e null =>
EXIST(b):[b e x & (a1,b) e nx]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e null & b1 e x & b2 e x
=>
[(a1,b1) e nx & (a1,b2) e nx => b1=b2]]
Join, 51, 50
53 EXIST(fun):ALL(a1):ALL(b):[a1 e null & b e x
=>
[fun(a1)=b <=> (a1,b) e nx]]
Detach, 33, 52
Define: f
(Function f defined in terms of graph set nx)
54 ALL(a1):ALL(b):[a1 e null & b e x
=>
[f(a1)=b <=> (a1,b) e nx]]
E Spec, 53
Prove: ALL(a):[a e null => f(a) e x] (f is an empty function)
Suppose...
55 t e null
Premise
Apply previous result
56 t e null => EXIST(b):[b e x & (t,b) e nx]
U Spec, 44
57 EXIST(b):[b e x & (t,b) e nx]
Detach, 56, 55
58 u e x & (t,u) e nx
E Spec, 57
59 u e x
Split, 58
60 (t,u) e nx
Split, 58
Apply definition of f
61 ALL(b):[t e null & b e x
=>
[f(t)=b <=> (t,b) e nx]]
U Spec, 54
62 t e null & u e x
=>
[f(t)=u <=> (t,u) e nx]
U Spec, 61
63 t e null & u e x
Join, 55, 59
64 f(t)=u <=> (t,u) e nx
Detach, 62, 63
65 [f(t)=u => (t,u) e nx] & [(t,u) e nx => f(t)=u]
Iff-And, 64
66 f(t)=u => (t,u) e nx
Split, 65
67 (t,u) e nx => f(t)=u
Split, 65
68 f(t)=u
Detach, 67, 60
69 f(t) e x
Substitute, 68,
59
As Required:
70 ALL(a):[a e null => f(a) e x]
4 Conclusion, 55
Prove: ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]
Suppose...
71 ALL(a):[a e null => g(a) e x]
Premise
Apply function equality axiom
72 ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a e null => f(a) e cod] & ALL(a):[a e null => g(a) e cod]
=>
[f=g <=> ALL(a):[a e null =>
f(a)=g(a)]]]
U Spec, 1
73 ALL(f):ALL(g):[Set(null) & Set(x) &
ALL(a):[a e null => f(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f=g <=> ALL(a):[a e null =>
f(a)=g(a)]]]
U Spec, 72
74 ALL(g):[Set(null) & Set(x) & ALL(a):[a e null => f(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f=g <=> ALL(a):[a e null => f(a)=g(a)]]]
U Spec, 73
75 Set(null) & Set(x) &
ALL(a):[a e null => f(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f=g <=> ALL(a):[a e null => f(a)=g(a)]]
U Spec, 74
76 Set(null) & Set(x)
Join, 2, 4
77 Set(null) & Set(x)
&
ALL(a):[a e null => f(a) e x]
Join, 76, 70
78 Set(null) & Set(x)
&
ALL(a):[a e null => f(a) e x]
&
ALL(a):[a e null => g(a) e x]
Join, 77, 71
79 f=g <=> ALL(a):[a e null => f(a)=g(a)]
Detach, 75, 78
80 [f=g => ALL(a):[a e null => f(a)=g(a)]]
&
[ALL(a):[a e null => f(a)=g(a)] => f=g]
Iff-And, 79
Sufficient: For f=g
81 ALL(a):[a e null => f(a)=g(a)] => f=g
Split, 80
Prove: ALL(t):[t e null => f(t)=g(t)]
Suppose...
82 t e null
Premise
83 ~t e null
U Spec, 3
84 ~t e null => f(t)=g(t)
Arb Cons, 82
85 f(t)=g(t)
Detach, 84, 83
As Required:
86 ALL(t):[t e null => f(t)=g(t)]
4 Conclusion, 82
87 f=g
Detach, 81, 86
88 g=f
Sym, 87
As Required:
89 ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]
4 Conclusion, 71
Joining results...
90 ALL(a):[a e null => f(a) e x]
&
ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]
Join, 70, 89
As Required:
91 ALL(x):[Set(x)
=>
EXIST(f):[ALL(a):[a e null => f(a) e x]
&
ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]]
4 Conclusion, 4
Suppose...
92 Set(x)
Premise
Apply Function Space Axiom
93 ALL(dom):ALL(cod):[Set(dom) & Set(cod)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e dom => f(a1) e cod]]]]
Fn Space
94 ALL(cod):[Set(null) & Set(cod)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e null => f(a1) e cod]]]]
U Spec, 93
95 Set(null) & Set(x)
=>
EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e null => f(a1) e x]]]
U Spec, 94
96 Set(null) & Set(x)
Join, 2, 92
97 EXIST(fsp):[Set(fsp) & ALL(f):[f e fsp <=> ALL(a1):[a1 e null => f(a1) e x]]]
Detach, 95, 96
98 Set(fs) & ALL(f):[f e fs <=> ALL(a1):[a1 e null => f(a1) e x]]
E Spec, 97
Define: fs
(function space)
99 Set(fs)
Split, 98
100 ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
Split, 98
Apply previous result
101 Set(x)
=>
EXIST(f):[ALL(a):[a e null => f(a) e x]
&
ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]
U Spec, 91
102 EXIST(f):[ALL(a):[a e null => f(a) e x]
&
ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]
Detach, 101, 92
103 EXIST(f):[ALL(a):[a e null => f(a) e x]
&
ALL(g):[ALL(a):[a e null => g(a) e x] => g=f]]
Detach, 101, 92
104 ALL(a):[a e null => f1(a) e x]
& ALL(g):[ALL(a):[a e null => g(a) e x] => g=f1]
E Spec, 103
From previous result (f1 is unique)
105 ALL(a):[a e null => f1(a) e x]
Split, 104
Apply definition of fs
106 f1 e fs <=> ALL(a1):[a1 e null => f1(a1) e x]
U Spec, 100
107 [f1 e fs => ALL(a1):[a1 e null => f1(a1) e x]]
&
[ALL(a1):[a1 e null => f1(a1) e x] => f1 e fs]
Iff-And, 106
108 ALL(a1):[a1 e null => f1(a1) e x] => f1 e fs
Split, 107
From definition of fs
109 f1 e fs
Detach, 108, 105
110 f2 e fs
Premise
111 f2 e fs <=> ALL(a1):[a1 e null => f2(a1) e x]
U Spec, 100
112 [f2 e fs => ALL(a1):[a1 e null => f2(a1) e x]]
&
[ALL(a1):[a1 e null => f2(a1) e x] => f2 e fs]
Iff-And, 111
113 f2 e fs => ALL(a1):[a1 e null => f2(a1) e x]
Split, 112
114 ALL(a1):[a1 e null => f2(a1) e x]
Detach, 113, 110
115 ALL(cod):ALL(f):ALL(g):[Set(null) & Set(cod) & ALL(a):[a e null => f(a) e cod] & ALL(a):[a e null => g(a) e cod]
=>
[f=g <=> ALL(a):[a e null =>
f(a)=g(a)]]]
U Spec, 1
116 ALL(f):ALL(g):[Set(null) & Set(x) &
ALL(a):[a e null => f(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f=g <=> ALL(a):[a e null =>
f(a)=g(a)]]]
U Spec, 115
117 ALL(g):[Set(null) & Set(x) & ALL(a):[a e null => f2(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f2=g <=> ALL(a):[a e null => f2(a)=g(a)]]]
U Spec, 116
118 Set(null) & Set(x) &
ALL(a):[a e null => f2(a) e x] & ALL(a):[a e null => f1(a) e x]
=>
[f2=f1 <=> ALL(a):[a e null => f2(a)=f1(a)]]
U Spec, 117
119 Set(null) & Set(x)
Join, 2, 92
120 Set(null) & Set(x)
&
ALL(a1):[a1 e null => f2(a1) e x]
Join, 119, 114
121 Set(null) & Set(x)
&
ALL(a1):[a1 e null => f2(a1) e x]
&
ALL(a):[a e null => f1(a) e x]
Join, 120, 105
122 f2=f1 <=> ALL(a):[a e null => f2(a)=f1(a)]
Detach, 118, 121
123 [f2=f1 => ALL(a):[a e null => f2(a)=f1(a)]]
&
[ALL(a):[a e null => f2(a)=f1(a)] => f2=f1]
Iff-And, 122
124 ALL(a):[a e null => f2(a)=f1(a)] => f2=f1
Split, 123
Suppose...
125 t e null
Premise
126 ~t e null
U Spec, 3
127 ~t e null => f2(t)=f1(t)
Arb Cons, 125
128 f2(t)=f1(t)
Detach, 127, 126
As Required:
129 ALL(a):[a e null => f2(a)=f1(a)]
4 Conclusion, 125
130 f2=f1
Detach, 124, 129
131 ALL(f2):[f2 e fs => f2=f1]
4 Conclusion, 110
132 Set(fs) & f1 e fs
Join, 99, 109
133 ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
&
ALL(f2):[f2 e fs => f2=f1]
Join, 100, 131
134 Set(fs) & f1 e fs
&
[ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
&
ALL(f2):[f2 e fs => f2=f1]]
Join, 132, 133
135 EXIST(f1):[Set(fs) & f1 e fs
&
[ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
&
ALL(f2):[f2 e fs => f2=f1]]]
E Gen, 134
136 EXIST(fs):EXIST(f1):[Set(fs) & f1 e fs
&
[ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
&
ALL(f2):[f2 e fs =>
f2=f1]]]
E Gen, 135
As Required:
137 ALL(x):[Set(x)
=>
EXIST(fs):EXIST(f1):[Set(fs) & f1 e fs
&
[ALL(f):[f e fs <=>
ALL(a1):[a1 e null => f(a1) e x]]
&
ALL(f2):[f2 e fs =>
f2=f1]]]]
4 Conclusion, 92