THEOREM
-------
Let f be an injective (one-to-one) function defined on a set s:
1-1
f: s ---> s
For every element s1 of s with no pre-image in s under f, there exists a unique set n
that is identical in structure to the set of natural numbers (as defined by Peano's axioms)
in which f is the successor function.
INFORMAL OUTLINE
----------------
We construct n = {s1, f(s1), f(f(s1)), ... }
The usual axioms for the natural numbers, with f as the successor function, are shown
here to apply on n:
N1: s1 e n (lines 12-21)
N2: ALL(a):[a e n => f(a) e n] (22-48)
N3: ALL(a):ALL(b):[a e n & b e n => [f(a)=f(b) => a=b]] (49-70)
N4: ALL(a):[a e n => ~f(a)=s1] (71-81)
N5: ALL(b):[Set(b) (82-106)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
The remainder of the proof establishes the uniqueness of n
This proof was prepared with the aid of the author's DC Proof 2.0 system
available free http://www.dcproof.com
PROOF
-----
Let f be an injective (one-to-one) function on s
1 Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
Premise
Splitting up this premise...
s is a set
2 Set(s)
Split, 1
f is a function mapping s to s
3 ALL(b):[b e s => f(b) e s]
Split, 1
f is an injective
4 ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
Split, 1
Suppose that s1 be an element of s with no pre-image under f
5 s1 e s & ALL(b):[b e s => ~f(b)=s1]
Premise
Splitting up this premise...
s1 is an element of s
6 s1 e s
Split, 5
s1 has no pre-image under f
7 ALL(b):[b e s => ~f(b)=s1]
Split, 5
Construct the set n
Applying the Subset Axiom...
8 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]]
Subset, 2
9 Set(n) & ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
E Spec, 8
Define: n
10 Set(n)
Split, 9
11 ALL(a):[a e n <=> a e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> a e b]]
Split, 9
PROVE N1
--------
Prove: s1 e n
Apply definition of n for s1
12 s1 e n <=> s1 e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]
U Spec, 11
13 [s1 e n => s1 e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]]
& [s1 e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b] => s1 e n]
Iff-And, 12
14 s1 e n => s1 e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]
Split, 13
Sufficient: For s1 e n
15 s1 e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b] => s1 e n
Split, 13
Prove: ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]
Suppose...
16 Set(p)
& s1 e p
& ALL(c):[c e p & c e s => f(c) e p]
Premise
17 Set(p)
Split, 16
18 s1 e p
Split, 16
As Required:
19 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]
4 Conclusion, 16
20 s1 e s
& ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> s1 e b]
Join, 6, 19
N1:
---
21 s1 e n
Detach, 15, 20
PROVE N2
--------
Prove: ALL(b):[b e n => f(b) e n]
Suppose...
22 x e n
Premise
Apply definition of n for x
23 x e n <=> x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 11
24 [x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 23
25 x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 24
26 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 24
27 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 25, 22
28 x e s
Split, 27
29 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 27
Apply definition of n for f(x)
30 f(x) e n <=> f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
U Spec, 11
31 [f(x) e n => f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]]
& [f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n]
Iff-And, 30
32 f(x) e n => f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Split, 31
Sufficient: For f(x) e n
33 f(x) e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b] => f(x) e n
Split, 31
34 x e s => f(x) e s
U Spec, 3
35 f(x) e s
Detach, 34, 28
Prove: ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Suppose...
36 Set(p)
& s1 e p
& ALL(c):[c e p & c e s => f(c) e p]
Premise
37 Set(p)
Split, 36
38 s1 e p
Split, 36
39 ALL(c):[c e p & c e s => f(c) e p]
Split, 36
From previous result
40 Set(p)
& s1 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 29
41 x e p
Detach, 40, 36
42 x e p & x e s => f(x) e p
U Spec, 39
43 x e p & x e s
Join, 41, 28
44 f(x) e p
Detach, 42, 43
As Required:
45 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
4 Conclusion, 36
46 f(x) e s
& ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> f(x) e b]
Join, 35, 45
47 f(x) e n
Detach, 33, 46
N2:
---
48 ALL(b):[b e n => f(b) e n]
4 Conclusion, 22
PROVE N3
--------
Prove: ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
Suppose...
49 x e n & y e n
Premise
50 x e n
Split, 49
51 y e n
Split, 49
Apply premise
52 ALL(c):[x e s & c e s => [f(x)=f(c) => x=c]]
U Spec, 4
53 x e s & y e s => [f(x)=f(y) => x=y]
U Spec, 52
Apply definition of n for x
54 x e n <=> x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 11
55 [x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 54
56 x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 55
57 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 55
58 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 56, 50
59 x e s
Split, 58
60 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 58
Apply definition of n for y
61 y e n <=> y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
U Spec, 11
62 [y e n => y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]]
& [y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b] => y e n]
Iff-And, 61
63 y e n => y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Split, 62
64 y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b] => y e n
Split, 62
65 y e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Detach, 63, 51
66 y e s
Split, 65
67 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> y e b]
Split, 65
68 x e s & y e s
Join, 59, 66
69 f(x)=f(y) => x=y
Detach, 53, 68
N3:
---
70 ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
4 Conclusion, 49
PROVE N4
--------
Prove: ALL(b):[b e n => ~f(b)=s1]
Suppose...
71 x e n
Premise
72 x e s => ~f(x)=s1
U Spec, 7
Apply definition of n for x
73 x e n <=> x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 11
74 [x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 73
75 x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 74
76 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 74
77 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 75, 71
78 x e s
Split, 77
79 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 77
80 ~f(x)=s1
Detach, 72, 78
N4:
---
81 ALL(b):[b e n => ~f(b)=s1]
4 Conclusion, 71
PROVE N5
--------
Prove: ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
Suppose...
82 Set(p)
& ALL(c):[c e p => c e n]
& s1 e p
& ALL(c):[c e p => f(c) e p]
Premise
83 Set(p)
Split, 82
84 ALL(c):[c e p => c e n]
Split, 82
85 s1 e p
Split, 82
How about ALL(c):[c e p & c e n => f(c) e p] ????
86 ALL(c):[c e p => f(c) e p]
Split, 82
Prove: ALL(c):[c e n => c e p]
Suppose...
87 x e n
Premise
Apply definiton of n for x
88 x e n <=> x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 11
89 [x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 88
90 x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 89
91 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 89
92 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 90, 87
93 x e s
Split, 92
94 ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 92
Sufficient: For x e p
95 Set(p)
& s1 e p
& ALL(c):[c e p & c e s => f(c) e p]
=> x e p
U Spec, 94
Prove: ALL(c):[c e p & c e s => f(c) e p]
Suppose...
96 y e p & y e s
Premise
97 y e p
Split, 96
98 y e s
Split, 96
Apply previous result
99 y e p => f(y) e p
U Spec, 86
100 f(y) e p
Detach, 99, 97
As Required:
101 ALL(c):[c e p & c e s => f(c) e p]
4 Conclusion, 96
102 Set(p) & s1 e p
Join, 83, 85
103 Set(p) & s1 e p
& ALL(c):[c e p & c e s => f(c) e p]
Join, 102, 101
104 x e p
Detach, 95, 103
As Required:
105 ALL(c):[c e n => c e p]
4 Conclusion, 87
N5:
---
The principle of mathematical induction holds on n
106 ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
4 Conclusion, 82
PROVE UNIQUENESS OF n
---------------------
Prove: ALL(b):[b e n => b e s]
Suppose...
107 x e n
Premise
108 x e n <=> x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
U Spec, 11
109 [x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]]
& [x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n]
Iff-And, 108
110 x e n => x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Split, 109
111 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b] => x e n
Split, 109
112 x e s & ALL(b):[Set(b)
& s1 e b
& ALL(c):[c e b & c e s => f(c) e b]
=> x e b]
Detach, 110, 107
113 x e s
Split, 112
As Required:
114 ALL(b):[b e n => b e s]
4 Conclusion, 107
115 Set(n) & ALL(b):[b e n => b e s]
Join, 10, 114
116 Set(n) & ALL(b):[b e n => b e s] & s1 e n
Join, 115, 21
117 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
Join, 116, 48
118 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
Join, 117, 70
119 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
Join, 118, 81
120 Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
Join, 119, 106
Prove: n'=n where...
121 Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
Premise
122 Set(n')
Split, 121
123 ALL(b):[b e n' => b e s]
Split, 121
124 s1 e n'
Split, 121
125 ALL(b):[b e n' => f(b) e n']
Split, 121
126 ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
Split, 121
127 ALL(b):[b e n' => ~f(b)=s1]
Split, 121
128 ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
Split, 121
129 Set(n')
& [Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]]
Join, 122, 120
Apply Set Equality Axiom
130 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
131 ALL(b):[Set(n') & Set(b) => [n'=b <=> ALL(c):[c e n' <=> c e b]]]
U Spec, 130
132 Set(n') & Set(n) => [n'=n <=> ALL(c):[c e n' <=> c e n]]
U Spec, 131
133 Set(n') & Set(n)
Join, 122, 10
134 n'=n <=> ALL(c):[c e n' <=> c e n]
Detach, 132, 133
135 [n'=n => ALL(c):[c e n' <=> c e n]]
& [ALL(c):[c e n' <=> c e n] => n'=n]
Iff-And, 134
136 n'=n => ALL(c):[c e n' <=> c e n]
Split, 135
Sufficient: n'=n
137 ALL(c):[c e n' <=> c e n] => n'=n
Split, 135
138 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n' & a e n]]
Subset, 122
139 Set(p) & ALL(a):[a e p <=> a e n' & a e n]
E Spec, 138
Define: p
140 Set(p)
Split, 139
141 ALL(a):[a e p <=> a e n' & a e n]
Split, 139
Sufficient: ALL(c):[c e n' => c e p]
142 Set(p)
& ALL(c):[c e p => c e n']
& s1 e p
& ALL(c):[c e p => f(c) e p]
=> ALL(c):[c e n' => c e p]
U Spec, 128
Prove: ALL(c):[c e p => c e n']
Suppose...
143 x e p
Premise
144 x e p <=> x e n' & x e n
U Spec, 141
145 [x e p => x e n' & x e n] & [x e n' & x e n => x e p]
Iff-And, 144
146 x e p => x e n' & x e n
Split, 145
147 x e n' & x e n => x e p
Split, 145
148 x e n' & x e n
Detach, 146, 143
149 x e n'
Split, 148
As Required:
150 ALL(c):[c e p => c e n']
4 Conclusion, 143
151 s1 e p <=> s1 e n' & s1 e n
U Spec, 141
152 [s1 e p => s1 e n' & s1 e n]
& [s1 e n' & s1 e n => s1 e p]
Iff-And, 151
153 s1 e p => s1 e n' & s1 e n
Split, 152
Sufficient: s1 e p
154 s1 e n' & s1 e n => s1 e p
Split, 152
155 s1 e n' & s1 e n
Join, 124, 21
As Required:
156 s1 e p
Detach, 154, 155
Prove: ALL(c):[c e p => f(c) e p]
Suppose...
157 x e p
Premise
158 x e p <=> x e n' & x e n
U Spec, 141
159 [x e p => x e n' & x e n] & [x e n' & x e n => x e p]
Iff-And, 158
160 x e p => x e n' & x e n
Split, 159
161 x e n' & x e n => x e p
Split, 159
162 x e n' & x e n
Detach, 160, 157
163 x e n'
Split, 162
164 x e n
Split, 162
165 f(x) e p <=> f(x) e n' & f(x) e n
U Spec, 141
166 [f(x) e p => f(x) e n' & f(x) e n]
& [f(x) e n' & f(x) e n => f(x) e p]
Iff-And, 165
167 f(x) e p => f(x) e n' & f(x) e n
Split, 166
Sufficient: f(x) e p
168 f(x) e n' & f(x) e n => f(x) e p
Split, 166
169 x e n' => f(x) e n'
U Spec, 125
170 f(x) e n'
Detach, 169, 163
171 x e n => f(x) e n
U Spec, 48
172 f(x) e n
Detach, 171, 164
173 f(x) e n' & f(x) e n
Join, 170, 172
174 f(x) e p
Detach, 168, 173
As Required:
175 ALL(c):[c e p => f(c) e p]
4 Conclusion, 157
176 Set(p) & ALL(c):[c e p => c e n']
Join, 140, 150
177 Set(p) & ALL(c):[c e p => c e n'] & s1 e p
Join, 176, 156
178 Set(p) & ALL(c):[c e p => c e n'] & s1 e p
& ALL(c):[c e p => f(c) e p]
Join, 177, 175
179 ALL(c):[c e n' => c e p]
Detach, 142, 178
Prove: ALL(c):[c e n' => c e n]
Suppose...
180 x e n'
Premise
181 x e n' => x e p
U Spec, 179
182 x e p
Detach, 181, 180
183 x e p <=> x e n' & x e n
U Spec, 141
184 [x e p => x e n' & x e n] & [x e n' & x e n => x e p]
Iff-And, 183
185 x e p => x e n' & x e n
Split, 184
186 x e n' & x e n => x e p
Split, 184
187 x e n' & x e n
Detach, 185, 182
188 x e n'
Split, 187
189 x e n
Split, 187
As Required:
190 ALL(c):[c e n' => c e n]
4 Conclusion, 180
191 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & a e n']]
Subset, 10
192 Set(p') & ALL(a):[a e p' <=> a e n & a e n']
E Spec, 191
Define: p'
193 Set(p')
Split, 192
194 ALL(a):[a e p' <=> a e n & a e n']
Split, 192
Sufficient: ALL(c):[c e n => c e p']
195 Set(p')
& ALL(c):[c e p' => c e n]
& s1 e p'
& ALL(c):[c e p' => f(c) e p']
=> ALL(c):[c e n => c e p']
U Spec, 106
Prove: ALL(c):[c e p' => c e n]
Suppose...
196 x e p'
Premise
197 x e p' <=> x e n & x e n'
U Spec, 194
198 [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']
Iff-And, 197
199 x e p' => x e n & x e n'
Split, 198
200 x e n & x e n' => x e p'
Split, 198
201 x e n & x e n'
Detach, 199, 196
202 x e n
Split, 201
As Required:
203 ALL(c):[c e p' => c e n]
4 Conclusion, 196
204 s1 e p' <=> s1 e n & s1 e n'
U Spec, 194
205 [s1 e p' => s1 e n & s1 e n']
& [s1 e n & s1 e n' => s1 e p']
Iff-And, 204
206 s1 e p' => s1 e n & s1 e n'
Split, 205
Sufficient: s1 e p'
207 s1 e n & s1 e n' => s1 e p'
Split, 205
208 s1 e n & s1 e n'
Join, 21, 124
As Required:
209 s1 e p'
Detach, 207, 208
Prove: ALL(c):[c e p' => f(c) e p']
Suppose...
210 x e p'
Premise
211 x e p' <=> x e n & x e n'
U Spec, 194
212 [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']
Iff-And, 211
213 x e p' => x e n & x e n'
Split, 212
214 x e n & x e n' => x e p'
Split, 212
215 x e n & x e n'
Detach, 213, 210
216 x e n
Split, 215
217 x e n'
Split, 215
218 f(x) e p' <=> f(x) e n & f(x) e n'
U Spec, 194
219 [f(x) e p' => f(x) e n & f(x) e n']
& [f(x) e n & f(x) e n' => f(x) e p']
Iff-And, 218
220 f(x) e p' => f(x) e n & f(x) e n'
Split, 219
221 f(x) e n & f(x) e n' => f(x) e p'
Split, 219
222 x e n => f(x) e n
U Spec, 48
223 f(x) e n
Detach, 222, 216
224 x e n' => f(x) e n'
U Spec, 125
225 f(x) e n'
Detach, 224, 217
226 f(x) e n & f(x) e n'
Join, 223, 225
227 f(x) e p'
Detach, 221, 226
As Required:
228 ALL(c):[c e p' => f(c) e p']
4 Conclusion, 210
229 Set(p') & ALL(c):[c e p' => c e n]
Join, 193, 203
230 Set(p') & ALL(c):[c e p' => c e n] & s1 e p'
Join, 229, 209
231 Set(p') & ALL(c):[c e p' => c e n] & s1 e p'
& ALL(c):[c e p' => f(c) e p']
Join, 230, 228
As Required:
232 ALL(c):[c e n => c e p']
Detach, 195, 231
Prove: ALL(c):[c e n => c e n']
Suppose...
233 x e n
Premise
234 x e n => x e p'
U Spec, 232
235 x e p'
Detach, 234, 233
236 x e p' <=> x e n & x e n'
U Spec, 194
237 [x e p' => x e n & x e n'] & [x e n & x e n' => x e p']
Iff-And, 236
238 x e p' => x e n & x e n'
Split, 237
239 x e n & x e n' => x e p'
Split, 237
240 x e n & x e n'
Detach, 238, 235
241 x e n
Split, 240
242 x e n'
Split, 240
As Required:
243 ALL(c):[c e n => c e n']
4 Conclusion, 233
244 ALL(c):[[c e n' => c e n] & [c e n => c e n']]
Join, 190, 243
245 ALL(c):[c e n' <=> c e n]
Iff-And, 244
246 n'=n
Detach, 137, 245
n is unique
As Required:
247 ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]
4 Conclusion, 121