THEOREM
*******
On every set, there is exists a
unique empty function
ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a
e null => f(a) e x]
& ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] &
ALL(a):[a e null => f2(a) e x] =>
f1=f2]]
OUTLINE
*******
1. Prove: EXIST(f):ALL(a):[a
e null => f(a) e x] (Line
1-71)
2. ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] &
ALL(a):[a e null => f2(a) e x] =>
f1=f2] (Line 72-95)
By Dan Christensen
2022-04-02
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
Prove: ALL(x):[Set(x)
=> EXIST(f):ALL(a):[a e null =>
f(a) e x]
&
ALL(f1):ALL(f2):[ALL(a):[a e null =>
f1(a) e x] & ALL(a):[a e null =>
f2(a) e x] => f1=f2]]
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)
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
(in terms of 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
As Required:
71 EXIST(f):ALL(a):[a e null => f(a) e x]
E Gen, 70
Prove: ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] &
ALL(a):[a e null => f2(a) e x] =>
f1=f2]
Suppose...
72 ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]
Premise
73 ALL(a):[a e null => f1(a) e x]
Split, 72
74 ALL(a):[a e null => f2(a) e x]
Split, 72
Apply definition of function equality
75 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
76 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, 75
77 ALL(g):[Set(null) & Set(x) & ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => g(a) e x]
=>
[f1=g <=> ALL(a):[a e null => f1(a)=g(a)]]]
U Spec, 76
78 Set(null) & Set(x) &
ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]
=>
[f1=f2 <=> ALL(a):[a e null => f1(a)=f2(a)]]
U Spec, 77
79 Set(null) & Set(x)
Join, 2, 4
80 Set(null) & Set(x)
&
ALL(a):[a e null => f1(a) e x]
Join, 79, 73
81 Set(null) & Set(x)
&
ALL(a):[a e null => f1(a) e x]
&
ALL(a):[a e null => f2(a) e x]
Join, 80, 74
82 f1=f2 <=> ALL(a):[a e null => f1(a)=f2(a)]
Detach, 78, 81
83 [f1=f2 => ALL(a):[a e null => f1(a)=f2(a)]]
&
[ALL(a):[a e null => f1(a)=f2(a)] => f1=f2]
Iff-And, 82
84 ALL(a):[a e null => f1(a)=f2(a)] => f1=f2
Split, 83
Prove: ALL(a):[a e null => f1(a)=f2(a)]
Suppose...
85 t e null
Premise
Apply definition of f1
86 t e null => f1(t) e x
U Spec, 73
87 f1(t) e x
Detach, 86, 85
Apply definition of f2
88 t e null => f2(t) e x
U Spec, 74
89 f2(t) e x
Detach, 88, 85
90 ~t e null
U Spec, 3
91 ~t e null => f1(t)=f2(t)
Arb Cons, 85
92 f1(t)=f2(t)
Detach, 91, 90
As Required:
93 ALL(a):[a e null => f1(a)=f2(a)]
4 Conclusion, 85
94 f1=f2
Detach, 84, 93
As Required:
95 ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]
=>
f1=f2]
4 Conclusion, 72
Joining results...
96 EXIST(f):ALL(a):[a e null => f(a) e x]
&
ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]
=>
f1=f2]
Join, 71, 95
As Required:
97 ALL(x):[Set(x)
=>
EXIST(f):ALL(a):[a e null => f(a) e x]
&
ALL(f1):ALL(f2):[ALL(a):[a e null => f1(a) e x] & ALL(a):[a e null => f2(a) e x]
=>
f1=f2]]
4 Conclusion, 4