THEOREM
*******
All functions mapping the empty
set to the same set are equal.
More formally:
ALL(x):[Set(x)
=> ALL(f):ALL(g):[ALL(a):[a e null => f(a) e x]&
ALL(a):[a e null => g(a) e x] =>
f=g]]
By Dan Christensen
2022-03-27
Homepage: http://www.dcproof.com
PROOF
*****
Define: Equality of functions
(1 variable)
Note that functions are
comparable here only if they have the same domain and codomain.
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
Suppose we have functons f: null
--> x and g: null --> x.
Both have the same domain and codomain, so they are comparabe.
5 ALL(a):[a e null => f(a) e x]
&
ALL(a):[a e null => g(a) e x]
Premise
6 ALL(a):[a e null => f(a) e x]
Split, 5
7 ALL(a):[a e null => g(a) e x]
Split, 5
Apply the definition of equality
8 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
9 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, 8
10 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, 9
11 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, 10
12 Set(null) & Set(x)
Join, 2, 4
13 Set(null) & Set(x)
&
ALL(a):[a e null => f(a) e x]
Join, 12, 6
14 Set(null) & Set(x)
&
ALL(a):[a e null => f(a) e x]
&
ALL(a):[a e null => g(a) e x]
Join, 13, 7
15 f=g <=> ALL(a):[a e null => f(a)=g(a)]
Detach, 11, 14
16 [f=g => ALL(a):[a e null => f(a)=g(a)]]
&
[ALL(a):[a e null => f(a)=g(a)] => f=g]
Iff-And, 15
Sufficient: For f=g
17 ALL(a):[a e null => f(a)=g(a)] => f=g
Split, 16
Suppose...
18 t e null
Premise
19 ~t e null
U Spec, 3
20 ~t e null => f(t)=g(t)
Arb Cons, 18
21 f(t)=g(t)
Detach, 20, 19
As Required:
22 ALL(a):[a e null => f(a)=g(a)]
4 Conclusion, 18
23 f=g
Detach, 17, 22
As Required:
24 ALL(f):ALL(g):[ALL(a):[a e null => f(a) e x]
&
ALL(a):[a e null => g(a) e x]
=>
f=g]
4 Conclusion, 5
As Required:
25 ALL(x):[Set(x)
=>
ALL(f):ALL(g):[ALL(a):[a e null => f(a) e x]
&
ALL(a):[a e null => g(a) e x]
=>
f=g]]
4 Conclusion, 4