THEOREM
*******
Given two Peano systems (n,next,0) and (n',next',0'), there exists f: n --> n' such that
1. f(0)=0'
2. ALL(a):[a e n => f(next(a))=next'(f(a))]]
Outline
*******
1. Construct nn', the Cartesian product of n and n' (lines 13 - 20)
2. Construct pnn', the power set of nn' (lines 21 - 26)
3. Construct f, a subset of nn' (lines 27 - 30)
4. Prove (0,0') e f (lines 31 - 48)
5. Prove ALL(a):ALL(b):[a e n & b e n' => [(a,b) e f => (next(a),next'(b)) e f]] (lines 49 - 90)
6. Prove f is a function (lines 91 - 620)
7. Prove f(0)=0' (lines 621 - 627)
8. Prove f(next(x))=next'(f(x)) (lines 628 - 684)
(This proof was written with the aid of the author's DC Proof 2.0 software available at
DEFINITIONS
***********
Peano system (n,0,next)
***********************
1 Set(n)
Axiom
2 0 e n
Axiom
next is a function on n
3 ALL(a):[a e n => next(a) e n]
Axiom
next is an injective (1-to-1) function
4 ALL(a):ALL(b):[a e n & b e n => [next(a)=next(b) => a=b]]
Axiom
0 has no predecessor under next
5 ALL(a):[a e n => ~next(a)=0]
Axiom
Principle of mathematical induction (PMI) for (n,0,next)
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [0 e a & ALL(b):[b e a => next(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
Peano system (n',0',next')
**************************
7 Set(n')
Axiom
8 0' e n'
Axiom
next' is a function on n'
9 ALL(a):[a e n' => next'(a) e n']
Axiom
next' is an injective (1-to-1) function
10 ALL(a):ALL(b):[a e n' & b e n' => [next'(a)=next'(b) => a=b]]
Axiom
0' has no predecessor under next'
11 ALL(a):[a e n' => ~next'(a)=0']
Axiom
Principle of mathematical induction (PMI) for (n',0',next')
12 ALL(a):[Set(a) & ALL(b):[b e a => b e n']
=> [0' e a & ALL(b):[b e a => next'(b) e a]
=> ALL(b):[b e n' => b e a]]]
Axiom
PROOF
*****
Construct Cartesian product of n and n'
Apply Cartesian product axiom
13 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
14 ALL(a2):[Set(n) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e a2]]]
U Spec, 13
15 Set(n) & Set(n') => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n']]
U Spec, 14
16 Set(n) & Set(n')
Join, 1, 7
17 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e n & c2 e n']]
Detach, 15, 16
18 Set'(nn') & ALL(c1):ALL(c2):[(c1,c2) e nn' <=> c1 e n & c2 e n']
E Spec, 17
Define: nn' Cartesian product of n and n'
***********
19 Set'(nn')
Split, 18
20 ALL(c1):ALL(c2):[(c1,c2) e nn' <=> c1 e n & c2 e n']
Split, 18
Construct power set of nn'
Apply Power Set Axiom
21 ALL(a):[Set'(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e a]]]]
Power Set
22 Set'(nn') => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e nn']]]
U Spec, 21
23 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e nn']]]
Detach, 22, 19
24 Set(pnn')
& ALL(c):[c e pnn' <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e nn']]
E Spec, 23
Define: pnn' Power set of nn'
************
25 Set(pnn')
Split, 24
26 ALL(c):[c e pnn' <=> Set'(c) & ALL(d1):ALL(d2):[(d1,d2) e c => (d1,d2) e nn']]
Split, 24
Construct subset of nn'
Apply Subset Axiom
27 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (a,b) e c]]]
Subset, 19
28 Set'(f) & ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (a,b) e c]]
E Spec, 27
Define: f (subset of nn')
*********
29 Set'(f)
Split, 28
30 ALL(a):ALL(b):[(a,b) e f <=> (a,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (a,b) e c]]
Split, 28
Prove: (0,0') e f
Apply definition of f
31 ALL(b):[(0,b) e f <=> (0,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,b) e c]]
U Spec, 30
32 (0,0') e f <=> (0,0') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]
U Spec, 31
33 [(0,0') e f => (0,0') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]]
& [(0,0') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c] => (0,0') e f]
Iff-And, 32
34 (0,0') e f => (0,0') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]
Split, 33
Sufficient: (0,0') e f
35 (0,0') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c] => (0,0') e f
Split, 33
Prove: (0,0') e nn'
36 ALL(c2):[(0,c2) e nn' <=> 0 e n & c2 e n']
U Spec, 20
37 (0,0') e nn' <=> 0 e n & 0' e n'
U Spec, 36
38 [(0,0') e nn' => 0 e n & 0' e n']
& [0 e n & 0' e n' => (0,0') e nn']
Iff-And, 37
39 (0,0') e nn' => 0 e n & 0' e n'
Split, 38
40 0 e n & 0' e n' => (0,0') e nn'
Split, 38
41 0 e n & 0' e n'
Join, 2, 8
As Required:
42 (0,0') e nn'
Detach, 40, 41
Prove: ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]
Suppose...
43 q e pnn'
& (0,0') e q
& ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
Premise
44 q e pnn'
Split, 43
45 (0,0') e q
Split, 43
As Required:
46 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]
4 Conclusion, 43
47 (0,0') e nn'
& ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,0') e c]
Join, 42, 46
As Required:
48 (0,0') e f
Detach, 35, 47
Prove: ALL(a):ALL(b):[a e n & b e n' => [(a,b) e f => (next(a),next'(b)) e f]]
Suppose...
49 x e n & y e n'
Premise
50 x e n
Split, 49
51 y e n'
Split, 49
Prove: (x,y) e f => (next(x),next'(y)) e f
Suppose...
52 (x,y) e f
Premise
53 ALL(b):[(x,b) e f <=> (x,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,b) e c]]
U Spec, 30
54 (x,y) e f <=> (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
U Spec, 53
55 [(x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]]
& [(x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f]
Iff-And, 54
56 (x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 55
57 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f
Split, 55
58 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Detach, 56, 52
59 (x,y) e nn'
Split, 58
60 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 58
61 ALL(b):[(next(x),b) e f <=> (next(x),b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),b) e c]]
U Spec, 30
62 (next(x),next'(y)) e f <=> (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
U Spec, 61
63 [(next(x),next'(y)) e f => (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]]
& [(next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c] => (next(x),next'(y)) e f]
Iff-And, 62
64 (next(x),next'(y)) e f => (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Split, 63
Sufficient: (next(x),next'(y)) e f
65 (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c] => (next(x),next'(y)) e f
Split, 63
66 ALL(c2):[(next(x),c2) e nn' <=> next(x) e n & c2 e n']
U Spec, 20
67 (next(x),next'(y)) e nn' <=> next(x) e n & next'(y) e n'
U Spec, 66
68 [(next(x),next'(y)) e nn' => next(x) e n & next'(y) e n']
& [next(x) e n & next'(y) e n' => (next(x),next'(y)) e nn']
Iff-And, 67
69 (next(x),next'(y)) e nn' => next(x) e n & next'(y) e n'
Split, 68
70 next(x) e n & next'(y) e n' => (next(x),next'(y)) e nn'
Split, 68
71 x e n => next(x) e n
U Spec, 3
72 next(x) e n
Detach, 71, 50
73 y e n' => next'(y) e n'
U Spec, 9
74 next'(y) e n'
Detach, 73, 51
75 next(x) e n & next'(y) e n'
Join, 72, 74
As Required:
76 (next(x),next'(y)) e nn'
Detach, 70, 75
Prove: ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Suppose...
77 q e pnn'
& (0,0') e q
& ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
Premise
78 q e pnn'
Split, 77
79 (0,0') e q
Split, 77
80 ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
Split, 77
Sufficient: (x,y) e q
81 q e pnn'
& (0,0') e q
& ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
=> (x,y) e q
U Spec, 60
82 (x,y) e q
Detach, 81, 77
83 ALL(e):[(x,e) e q => (next(x),next'(e)) e q]
U Spec, 80
84 (x,y) e q => (next(x),next'(y)) e q
U Spec, 83
85 (next(x),next'(y)) e q
Detach, 84, 82
As Required:
86 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
4 Conclusion, 77
87 (next(x),next'(y)) e nn'
& ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Join, 76, 86
88 (next(x),next'(y)) e f
Detach, 65, 87
As Required:
89 (x,y) e f => (next(x),next'(y)) e f
4 Conclusion, 52
As Required:
90 ALL(a):ALL(b):[a e n & b e n' => [(a,b) e f => (next(a),next'(b)) e f]]
4 Conclusion, 49
Prove: f is a function
Apply Function Axiom
91 ALL(f):ALL(a):ALL(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):[d=f(c) <=> (c,d) e f]]
Function
92 ALL(a):ALL(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):[d=f(c) <=> (c,d) e f]]
U Spec, 91
93 ALL(b):[ALL(c):ALL(d):[(c,d) e f => c e n & d e b]
& ALL(c):[c e n => 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):[d=f(c) <=> (c,d) e f]]
U Spec, 92
Sufficient: For functionality of f (3 parts)
94 ALL(c):ALL(d):[(c,d) e f => c e n & d e n']
& ALL(c):[c e n => EXIST(d):[d e n' & (c,d) e f]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f & (c,d2) e f => d1=d2]
=> ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]
U Spec, 93
Prove: ALL(a):ALL(b):[(a,b) e f => a e n & b e n']
Suppose...
95 (x,y) e f
Premise
96 ALL(b):[(x,b) e f <=> (x,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,b) e c]]
U Spec, 30
97 (x,y) e f <=> (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
U Spec, 96
98 [(x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]]
& [(x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f]
Iff-And, 97
99 (x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 98
100 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f
Split, 98
101 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Detach, 99, 95
102 (x,y) e nn'
Split, 101
103 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 101
104 ALL(c2):[(x,c2) e nn' <=> x e n & c2 e n']
U Spec, 20
105 (x,y) e nn' <=> x e n & y e n'
U Spec, 104
106 [(x,y) e nn' => x e n & y e n']
& [x e n & y e n' => (x,y) e nn']
Iff-And, 105
107 (x,y) e nn' => x e n & y e n'
Split, 106
108 x e n & y e n' => (x,y) e nn'
Split, 106
109 x e n & y e n'
Detach, 107, 102
As Required: Functionality, Part 1
110 ALL(a):ALL(b):[(a,b) e f => a e n & b e n']
4 Conclusion, 95
111 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & EXIST(b):[b e n' & (a,b) e f]]]
Subset, 1
112 Set(p1) & ALL(a):[a e p1 <=> a e n & EXIST(b):[b e n' & (a,b) e f]]
E Spec, 111
Define: p1
113 Set(p1)
Split, 112
114 ALL(a):[a e p1 <=> a e n & EXIST(b):[b e n' & (a,b) e f]]
Split, 112
115 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 6
Prove: ALL(a):[a e p1 => a e n]
Suppose...
116 x e p1
Premise
117 x e p1 <=> x e n & EXIST(b):[b e n' & (x,b) e f]
U Spec, 114
118 [x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]]
& [x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1]
Iff-And, 117
119 x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]
Split, 118
120 x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1
Split, 118
121 x e n & EXIST(b):[b e n' & (x,b) e f]
Detach, 119, 116
122 x e n
Split, 121
As Required:
123 ALL(a):[a e p1 => a e n]
4 Conclusion, 116
124 Set(p1) & ALL(a):[a e p1 => a e n]
Join, 113, 123
Sufficient: ALL(b):[b e n => b e p1]
125 0 e p1 & ALL(b):[b e p1 => next(b) e p1]
=> ALL(b):[b e n => b e p1]
Detach, 115, 124
126 0 e p1 <=> 0 e n & EXIST(b):[b e n' & (0,b) e f]
U Spec, 114
127 [0 e p1 => 0 e n & EXIST(b):[b e n' & (0,b) e f]]
& [0 e n & EXIST(b):[b e n' & (0,b) e f] => 0 e p1]
Iff-And, 126
128 0 e p1 => 0 e n & EXIST(b):[b e n' & (0,b) e f]
Split, 127
Sufficient: 0 e p1
129 0 e n & EXIST(b):[b e n' & (0,b) e f] => 0 e p1
Split, 127
130 0' e n' & (0,0') e f
Join, 8, 48
131 EXIST(b):[b e n' & (0,b) e f]
E Gen, 130
132 0 e n & EXIST(b):[b e n' & (0,b) e f]
Join, 2, 131
As Required:
133 0 e p1
Detach, 129, 132
Prove: ALL(a):[a e p1 => next(a) e p1]
Suppose...
134 x e p1
Premise
135 x e p1 <=> x e n & EXIST(b):[b e n' & (x,b) e f]
U Spec, 114
136 [x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]]
& [x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1]
Iff-And, 135
137 x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]
Split, 136
138 x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1
Split, 136
139 x e n & EXIST(b):[b e n' & (x,b) e f]
Detach, 137, 134
140 x e n
Split, 139
141 EXIST(b):[b e n' & (x,b) e f]
Split, 139
142 y e n' & (x,y) e f
E Spec, 141
143 y e n'
Split, 142
144 (x,y) e f
Split, 142
145 next(x) e p1 <=> next(x) e n & EXIST(b):[b e n' & (next(x),b) e f]
U Spec, 114
146 [next(x) e p1 => next(x) e n & EXIST(b):[b e n' & (next(x),b) e f]]
& [next(x) e n & EXIST(b):[b e n' & (next(x),b) e f] => next(x) e p1]
Iff-And, 145
147 next(x) e p1 => next(x) e n & EXIST(b):[b e n' & (next(x),b) e f]
Split, 146
Sufficient: next(x) e p1
148 next(x) e n & EXIST(b):[b e n' & (next(x),b) e f] => next(x) e p1
Split, 146
149 x e n => next(x) e n
U Spec, 3
150 next(x) e n
Detach, 149, 140
151 ALL(b):[x e n & b e n' => [(x,b) e f => (next(x),next'(b)) e f]]
U Spec, 90
152 x e n & y e n' => [(x,y) e f => (next(x),next'(y)) e f]
U Spec, 151
153 x e n & y e n'
Join, 140, 143
154 (x,y) e f => (next(x),next'(y)) e f
Detach, 152, 153
155 (next(x),next'(y)) e f
Detach, 154, 144
156 y e n' => next'(y) e n'
U Spec, 9
157 next'(y) e n'
Detach, 156, 143
158 next'(y) e n' & (next(x),next'(y)) e f
Join, 157, 155
159 EXIST(b):[b e n' & (next(x),b) e f]
E Gen, 158
160 next(x) e n & EXIST(b):[b e n' & (next(x),b) e f]
Join, 150, 159
161 next(x) e p1
Detach, 148, 160
As Required:
162 ALL(a):[a e p1 => next(a) e p1]
4 Conclusion, 134
163 0 e p1 & ALL(a):[a e p1 => next(a) e p1]
Join, 133, 162
164 ALL(b):[b e n => b e p1]
Detach, 125, 163
Prove: ALL(a):[a e n => EXIST(b):[b e n' & (a,b) e f]]
Suppose...
165 x e n
Premise
166 x e n => x e p1
U Spec, 164
167 x e p1
Detach, 166, 165
168 x e p1 <=> x e n & EXIST(b):[b e n' & (x,b) e f]
U Spec, 114
169 [x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]]
& [x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1]
Iff-And, 168
170 x e p1 => x e n & EXIST(b):[b e n' & (x,b) e f]
Split, 169
171 x e n & EXIST(b):[b e n' & (x,b) e f] => x e p1
Split, 169
172 x e n & EXIST(b):[b e n' & (x,b) e f]
Detach, 170, 167
173 x e n
Split, 172
174 EXIST(b):[b e n' & (x,b) e f]
Split, 172
As Required: Functionality, Part 2
175 ALL(a):[a e n => EXIST(b):[b e n' & (a,b) e f]]
4 Conclusion, 165
Prove: ALL(a):[a e n' => [(0,a) e f => a=0']]
Suppose...
176 y e n'
Premise
Prove: (0,y)ef => y=0'
Suppose to the contrary...
177 (0,y) e f & ~y=0'
Premise
178 (0,y) e f
Split, 177
179 ~y=0'
Split, 177
180 ALL(b):[(0,b) e f <=> (0,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,b) e c]]
U Spec, 30
181 (0,y) e f <=> (0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c]
U Spec, 180
182 [(0,y) e f => (0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c]]
& [(0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c] => (0,y) e f]
Iff-And, 181
183 (0,y) e f => (0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c]
Split, 182
184 (0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c] => (0,y) e f
Split, 182
185 ~[(0,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y) e c]] => ~(0,y) e f
Contra, 183
186 ~[(0,y) e nn' & ALL(c):~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c]] => ~(0,y) e f
Imply-And, 185
187 ~~[~(0,y) e nn' | ~ALL(c):~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c]] => ~(0,y) e f
DeMorgan, 186
188 ~(0,y) e nn' | ~ALL(c):~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c] => ~(0,y) e f
Rem DNeg, 187
189 ~(0,y) e nn' | ~~EXIST(c):~~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c] => ~(0,y) e f
Quant, 188
190 ~(0,y) e nn' | EXIST(c):~~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c] => ~(0,y) e f
Rem DNeg, 189
Sufficient: ~(0,y) e f (to obtain a contradiction)
Use c=f' as defined below
191 ~(0,y) e nn' | EXIST(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(0,y) e c] => ~(0,y) e f
Rem DNeg, 190
192 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e f & ~[a=0 & b=y]]]
Subset, 29
193 Set'(f') & ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e f & ~[a=0 & b=y]]
E Spec, 192
Define: f' Subset of f
194 Set'(f')
Split, 193
195 ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e f & ~[a=0 & b=y]]
Split, 193
196 f' e pnn' <=> Set'(f') & ALL(d1):ALL(d2):[(d1,d2) e f' => (d1,d2) e nn']
U Spec, 26
197 [f' e pnn' => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) e f' => (d1,d2) e nn']]
& [Set'(f') & ALL(d1):ALL(d2):[(d1,d2) e f' => (d1,d2) e nn'] => f' e pnn']
Iff-And, 196
198 f' e pnn' => Set'(f') & ALL(d1):ALL(d2):[(d1,d2) e f' => (d1,d2) e nn']
Split, 197
Sufficient: f' e pnn'
199 Set'(f') & ALL(d1):ALL(d2):[(d1,d2) e f' => (d1,d2) e nn'] => f' e pnn'
Split, 197
Prove: ALL(a):ALL(b):[(a,b) e f' => (a,b) e nn']
Suppose...
200 (t,u) e f'
Premise
201 ALL(b):[(t,b) e f' <=> (t,b) e f & ~[t=0 & b=y]]
U Spec, 195
202 (t,u) e f' <=> (t,u) e f & ~[t=0 & u=y]
U Spec, 201
203 [(t,u) e f' => (t,u) e f & ~[t=0 & u=y]]
& [(t,u) e f & ~[t=0 & u=y] => (t,u) e f']
Iff-And, 202
204 (t,u) e f' => (t,u) e f & ~[t=0 & u=y]
Split, 203
205 (t,u) e f & ~[t=0 & u=y] => (t,u) e f'
Split, 203
206 (t,u) e f & ~[t=0 & u=y]
Detach, 204, 200
207 (t,u) e f
Split, 206
208 ~[t=0 & u=y]
Split, 206
209 ALL(b):[(t,b) e f <=> (t,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,b) e c]]
U Spec, 30
210 (t,u) e f <=> (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
U Spec, 209
211 [(t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]]
& [(t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f]
Iff-And, 210
212 (t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 211
213 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f
Split, 211
214 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Detach, 212, 207
215 (t,u) e nn'
Split, 214
As Required:
216 ALL(a):ALL(b):[(a,b) e f' => (a,b) e nn']
4 Conclusion, 200
217 Set'(f')
& ALL(a):ALL(b):[(a,b) e f' => (a,b) e nn']
Join, 194, 216
As Required:
218 f' e pnn'
Detach, 199, 217
219 ALL(b):[(0,b) e f' <=> (0,b) e f & ~[0=0 & b=y]]
U Spec, 195
220 (0,0') e f' <=> (0,0') e f & ~[0=0 & 0'=y]
U Spec, 219
221 [(0,0') e f' => (0,0') e f & ~[0=0 & 0'=y]]
& [(0,0') e f & ~[0=0 & 0'=y] => (0,0') e f']
Iff-And, 220
222 (0,0') e f' => (0,0') e f & ~[0=0 & 0'=y]
Split, 221
Sufficient: (0,0') e f'
223 (0,0') e f & ~[0=0 & 0'=y] => (0,0') e f'
Split, 221
Prove: ~[0=0 & 0'=y]
Suppose to the contrary...
224 0=0 & 0'=y
Premise
225 0=0
Split, 224
226 0'=y
Split, 224
227 y=0'
Sym, 226
228 y=0' & ~y=0'
Join, 227, 179
As Required:
229 ~[0=0 & 0'=y]
4 Conclusion, 224
230 (0,0') e f & ~[0=0 & 0'=y]
Join, 48, 229
As Required:
231 (0,0') e f'
Detach, 223, 230
Prove: ALL(a):ALL(b):[(a,b) e f' => (next(a),next'(b)) e f']
Suppose...
232 (t,u) e f'
Premise
233 ALL(b):[(t,b) e f' <=> (t,b) e f & ~[t=0 & b=y]]
U Spec, 195
234 (t,u) e f' <=> (t,u) e f & ~[t=0 & u=y]
U Spec, 233
235 [(t,u) e f' => (t,u) e f & ~[t=0 & u=y]]
& [(t,u) e f & ~[t=0 & u=y] => (t,u) e f']
Iff-And, 234
236 (t,u) e f' => (t,u) e f & ~[t=0 & u=y]
Split, 235
237 (t,u) e f & ~[t=0 & u=y] => (t,u) e f'
Split, 235
238 (t,u) e f & ~[t=0 & u=y]
Detach, 236, 232
239 (t,u) e f
Split, 238
240 ~[t=0 & u=y]
Split, 238
241 ALL(b):[(t,b) e f <=> (t,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,b) e c]]
U Spec, 30
242 (t,u) e f <=> (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
U Spec, 241
243 [(t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]]
& [(t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f]
Iff-And, 242
244 (t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 243
245 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f
Split, 243
246 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Detach, 244, 239
247 (t,u) e nn'
Split, 246
248 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 246
249 ALL(c2):[(t,c2) e nn' <=> t e n & c2 e n']
U Spec, 20
250 (t,u) e nn' <=> t e n & u e n'
U Spec, 249
251 [(t,u) e nn' => t e n & u e n']
& [t e n & u e n' => (t,u) e nn']
Iff-And, 250
252 (t,u) e nn' => t e n & u e n'
Split, 251
253 t e n & u e n' => (t,u) e nn'
Split, 251
254 t e n & u e n'
Detach, 252, 247
255 t e n
Split, 254
256 u e n'
Split, 254
257 ALL(b):[(next(t),b) e f' <=> (next(t),b) e f & ~[next(t)=0 & b=y]]
U Spec, 195
258 (next(t),next'(u)) e f' <=> (next(t),next'(u)) e f & ~[next(t)=0 & next'(u)=y]
U Spec, 257
259 [(next(t),next'(u)) e f' => (next(t),next'(u)) e f & ~[next(t)=0 & next'(u)=y]]
& [(next(t),next'(u)) e f & ~[next(t)=0 & next'(u)=y] => (next(t),next'(u)) e f']
Iff-And, 258
260 (next(t),next'(u)) e f' => (next(t),next'(u)) e f & ~[next(t)=0 & next'(u)=y]
Split, 259
Sufficient: (next(t),next'(u)) e f'
261 (next(t),next'(u)) e f & ~[next(t)=0 & next'(u)=y] => (next(t),next'(u)) e f'
Split, 259
262 ALL(b):[t e n & b e n' => [(t,b) e f => (next(t),next'(b)) e f]]
U Spec, 90
263 t e n & u e n' => [(t,u) e f => (next(t),next'(u)) e f]
U Spec, 262
264 (t,u) e f => (next(t),next'(u)) e f
Detach, 263, 254
265 (next(t),next'(u)) e f
Detach, 264, 239
Prove: ~[next(t)=0 & next'(u)=y]
Suppose to the contrary...
266 next(t)=0 & next'(u)=y
Premise
267 next(t)=0
Split, 266
268 next'(u)=y
Split, 266
269 t e n => ~next(t)=0
U Spec, 5
270 ~next(t)=0
Detach, 269, 255
271 next(t)=0 & ~next(t)=0
Join, 267, 270
As Required:
272 ~[next(t)=0 & next'(u)=y]
4 Conclusion, 266
273 (next(t),next'(u)) e f
& ~[next(t)=0 & next'(u)=y]
Join, 265, 272
274 (next(t),next'(u)) e f'
Detach, 261, 273
As Required:
275 ALL(a):ALL(b):[(a,b) e f' => (next(a),next'(b)) e f']
4 Conclusion, 232
276 ALL(b):[(0,b) e f' <=> (0,b) e f & ~[0=0 & b=y]]
U Spec, 195
277 (0,y) e f' <=> (0,y) e f & ~[0=0 & y=y]
U Spec, 276
278 [(0,y) e f' => (0,y) e f & ~[0=0 & y=y]]
& [(0,y) e f & ~[0=0 & y=y] => (0,y) e f']
Iff-And, 277
279 (0,y) e f' => (0,y) e f & ~[0=0 & y=y]
Split, 278
280 (0,y) e f & ~[0=0 & y=y] => (0,y) e f'
Split, 278
281 ~[(0,y) e f & ~[0=0 & y=y]] => ~(0,y) e f'
Contra, 279
282 ~~[~(0,y) e f | ~~[0=0 & y=y]] => ~(0,y) e f'
DeMorgan, 281
283 ~(0,y) e f | ~~[0=0 & y=y] => ~(0,y) e f'
Rem DNeg, 282
Sufficient: ~(0,y) e f'
284 ~(0,y) e f | 0=0 & y=y => ~(0,y) e f'
Rem DNeg, 283
285 0=0
Reflex
286 y=y
Reflex
287 0=0 & y=y
Join, 285, 286
288 ~(0,y) e f | 0=0 & y=y
Arb Or, 287
As Required:
289 ~(0,y) e f'
Detach, 284, 288
290 f' e pnn' & (0,0') e f'
Join, 218, 231
291 f' e pnn' & (0,0') e f'
& ALL(a):ALL(b):[(a,b) e f' => (next(a),next'(b)) e f']
Join, 290, 275
292 f' e pnn' & (0,0') e f'
& ALL(a):ALL(b):[(a,b) e f' => (next(a),next'(b)) e f']
& ~(0,y) e f'
Join, 291, 289
293 EXIST(c):[c e pnn' & (0,0') e c
& ALL(a):ALL(b):[(a,b) e c => (next(a),next'(b)) e c]
& ~(0,y) e c]
E Gen, 292
294 ~(0,y) e nn' | EXIST(c):[c e pnn' & (0,0') e c
& ALL(a):ALL(b):[(a,b) e c => (next(a),next'(b)) e c]
& ~(0,y) e c]
Arb Or, 293
As Required:
295 ~(0,y) e f
Detach, 191, 294
296 (0,y) e f & ~(0,y) e f
Join, 178, 295
As Required:
297 ~[(0,y) e f & ~y=0']
4 Conclusion, 177
298 ~~[(0,y) e f => ~~y=0']
Imply-And, 297
299 (0,y) e f => ~~y=0'
Rem DNeg, 298
300 (0,y) e f => y=0'
Rem DNeg, 299
As Required:
301 ALL(a):[a e n' => [(0,a) e f => a=0']]
4 Conclusion, 176
302 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]]
Subset, 1
303 Set(p2) & ALL(a):[a e p2 <=> a e n & ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
E Spec, 302
Define: p2
304 Set(p2)
Split, 303
305 ALL(a):[a e p2 <=> a e n & ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Split, 303
306 Set(p2) & ALL(b):[b e p2 => b e n]
=> [0 e p2 & ALL(b):[b e p2 => next(b) e p2]
=> ALL(b):[b e n => b e p2]]
U Spec, 6
Prove: ALL(a):[a e p2 => a e n]
Suppose...
307 x e p2
Premise
308 x e p2 <=> x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
U Spec, 305
309 [x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]]
& [x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2]
Iff-And, 308
310 x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Split, 309
311 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2
Split, 309
312 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Detach, 310, 307
313 x e n
Split, 312
As Required:
314 ALL(a):[a e p2 => a e n]
4 Conclusion, 307
315 Set(p2) & ALL(a):[a e p2 => a e n]
Join, 304, 314
Sufficient: ALL(b):[b e n => b e p2]
316 0 e p2 & ALL(b):[b e p2 => next(b) e p2]
=> ALL(b):[b e n => b e p2]
Detach, 306, 315
317 0 e p2 <=> 0 e n & ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]
U Spec, 305
318 [0 e p2 => 0 e n & ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]]
& [0 e n & ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2] => 0 e p2]
Iff-And, 317
319 0 e p2 => 0 e n & ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]
Split, 318
Sufficient: 0 e p2
320 0 e n & ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2] => 0 e p2
Split, 318
Prove: ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]
Suppose...
321 (0,y1) e f & (0,y2) e f
Premise
322 (0,y1) e f
Split, 321
323 (0,y2) e f
Split, 321
324 ALL(b):[(0,b) e f <=> (0,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,b) e c]]
U Spec, 30
325 (0,y1) e f <=> (0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c]
U Spec, 324
326 [(0,y1) e f => (0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c]]
& [(0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c] => (0,y1) e f]
Iff-And, 325
327 (0,y1) e f => (0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c]
Split, 326
328 (0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c] => (0,y1) e f
Split, 326
329 (0,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c]
Detach, 327, 322
330 (0,y1) e nn'
Split, 329
331 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y1) e c]
Split, 329
332 ALL(c2):[(0,c2) e nn' <=> 0 e n & c2 e n']
U Spec, 20
333 (0,y1) e nn' <=> 0 e n & y1 e n'
U Spec, 332
334 [(0,y1) e nn' => 0 e n & y1 e n']
& [0 e n & y1 e n' => (0,y1) e nn']
Iff-And, 333
335 (0,y1) e nn' => 0 e n & y1 e n'
Split, 334
336 0 e n & y1 e n' => (0,y1) e nn'
Split, 334
337 0 e n & y1 e n'
Detach, 335, 330
338 0 e n
Split, 337
339 y1 e n'
Split, 337
340 (0,y2) e f <=> (0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c]
U Spec, 324
341 [(0,y2) e f => (0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c]]
& [(0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c] => (0,y2) e f]
Iff-And, 340
342 (0,y2) e f => (0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c]
Split, 341
343 (0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c] => (0,y2) e f
Split, 341
344 (0,y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c]
Detach, 342, 323
345 (0,y2) e nn'
Split, 344
346 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (0,y2) e c]
Split, 344
347 (0,y2) e nn' <=> 0 e n & y2 e n'
U Spec, 332
348 [(0,y2) e nn' => 0 e n & y2 e n']
& [0 e n & y2 e n' => (0,y2) e nn']
Iff-And, 347
349 (0,y2) e nn' => 0 e n & y2 e n'
Split, 348
350 0 e n & y2 e n' => (0,y2) e nn'
Split, 348
351 0 e n & y2 e n'
Detach, 349, 345
352 0 e n
Split, 351
353 y2 e n'
Split, 351
354 y1 e n' => [(0,y1) e f => y1=0']
U Spec, 301
355 (0,y1) e f => y1=0'
Detach, 354, 339
356 y1=0'
Detach, 355, 322
357 y2 e n' => [(0,y2) e f => y2=0']
U Spec, 301
358 (0,y2) e f => y2=0'
Detach, 357, 353
359 y2=0'
Detach, 358, 323
360 y1=y2
Substitute, 359, 356
As Required:
361 ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]
4 Conclusion, 321
362 0 e n
& ALL(b1):ALL(b2):[(0,b1) e f & (0,b2) e f => b1=b2]
Join, 2, 361
As Required:
363 0 e p2
Detach, 320, 362
Prove: ALL(a):[a e p2 => next(a) e p2]
Suppose...
364 x e p2
Premise
365 x e p2 <=> x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
U Spec, 305
366 [x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]]
& [x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2]
Iff-And, 365
367 x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Split, 366
368 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2
Split, 366
369 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Detach, 367, 364
370 x e n
Split, 369
371 ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Split, 369
372 next(x) e p2 <=> next(x) e n & ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]
U Spec, 305
373 [next(x) e p2 => next(x) e n & ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]]
& [next(x) e n & ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2] => next(x) e p2]
Iff-And, 372
374 next(x) e p2 => next(x) e n & ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]
Split, 373
Sufficient: next(x) e p2
375 next(x) e n & ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2] => next(x) e p2
Split, 373
376 x e n => next(x) e n
U Spec, 3
377 next(x) e n
Detach, 376, 370
378 x e n => EXIST(b):[b e n' & (x,b) e f]
U Spec, 175
379 EXIST(b):[b e n' & (x,b) e f]
Detach, 378, 370
380 y e n' & (x,y) e f
E Spec, 379
381 y e n'
Split, 380
382 (x,y) e f
Split, 380
y is the unique image of x under f
383 ALL(b2):[(x,y) e f & (x,b2) e f => y=b2]
U Spec, 371
Prove: ALL(c):[c e n' => [(next(x),c) e f => c=next'(y)]]
Suppose...
384 y' e n'
Premise
Prove: ~[(next(x),y') e f & ~y'=next'(y)]
Suppose to the contrary...
385 (next(x),y') e f & ~y'=next'(y)
Premise
386 (next(x),y') e f
Split, 385
387 ~y'=next'(y)
Split, 385
388 ALL(b):[(next(x),b) e f <=> (next(x),b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),b) e c]]
U Spec, 30
389 (next(x),y') e f <=> (next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c]
U Spec, 388
390 [(next(x),y') e f => (next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c]]
& [(next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c] => (next(x),y') e f]
Iff-And, 389
391 (next(x),y') e f => (next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c]
Split, 390
392 (next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c] => (next(x),y') e f
Split, 390
393 ~[(next(x),y') e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c]] => ~(next(x),y') e f
Contra, 391
394 ~~[~(next(x),y') e nn' | ~ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c]] => ~(next(x),y') e f
DeMorgan, 393
395 ~(next(x),y') e nn' | ~ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c] => ~(next(x),y') e f
Rem DNeg, 394
396 ~(next(x),y') e nn' | ~~EXIST(c):~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c] => ~(next(x),y') e f
Quant, 395
397 ~(next(x),y') e nn' | EXIST(c):~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y') e c] => ~(next(x),y') e f
Rem DNeg, 396
398 ~(next(x),y') e nn' | EXIST(c):~~[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(next(x),y') e c] => ~(next(x),y') e f
Imply-And, 397
Sufficient: ~(next(x),y') e f (to obtain a contradiction)
Use c=f'' as defined below
399 ~(next(x),y') e nn' | EXIST(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c] & ~(next(x),y') e c] => ~(next(x),y') e f
Rem DNeg, 398
400 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e f & ~[a=next(x) & b=y']]]
Subset, 29
401 Set'(f'') & ALL(a):ALL(b):[(a,b) e f'' <=> (a,b) e f & ~[a=next(x) & b=y']]
E Spec, 400
Define: f''
***********
402 Set'(f'')
Split, 401
403 ALL(a):ALL(b):[(a,b) e f'' <=> (a,b) e f & ~[a=next(x) & b=y']]
Split, 401
404 f'' e pnn' <=> Set'(f'') & ALL(d1):ALL(d2):[(d1,d2) e f'' => (d1,d2) e nn']
U Spec, 26
405 [f'' e pnn' => Set'(f'') & ALL(d1):ALL(d2):[(d1,d2) e f'' => (d1,d2) e nn']]
& [Set'(f'') & ALL(d1):ALL(d2):[(d1,d2) e f'' => (d1,d2) e nn'] => f'' e pnn']
Iff-And, 404
406 f'' e pnn' => Set'(f'') & ALL(d1):ALL(d2):[(d1,d2) e f'' => (d1,d2) e nn']
Split, 405
Sufficient: f'' e pnn'
407 Set'(f'') & ALL(d1):ALL(d2):[(d1,d2) e f'' => (d1,d2) e nn'] => f'' e pnn'
Split, 405
Prove: ALL(a):ALL(b):[(a,b) e f'' => (a,b) e nn']
Suppose...
408 (t,u) e f''
Premise
409 ALL(b):[(t,b) e f'' <=> (t,b) e f & ~[t=next(x) & b=y']]
U Spec, 403
410 (t,u) e f'' <=> (t,u) e f & ~[t=next(x) & u=y']
U Spec, 409
411 [(t,u) e f'' => (t,u) e f & ~[t=next(x) & u=y']]
& [(t,u) e f & ~[t=next(x) & u=y'] => (t,u) e f'']
Iff-And, 410
412 (t,u) e f'' => (t,u) e f & ~[t=next(x) & u=y']
Split, 411
413 (t,u) e f & ~[t=next(x) & u=y'] => (t,u) e f''
Split, 411
414 (t,u) e f & ~[t=next(x) & u=y']
Detach, 412, 408
415 (t,u) e f
Split, 414
416 ~[t=next(x) & u=y']
Split, 414
417 ALL(b):[(t,b) e f <=> (t,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,b) e c]]
U Spec, 30
418 (t,u) e f <=> (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
U Spec, 417
419 [(t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]]
& [(t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f]
Iff-And, 418
420 (t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 419
421 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f
Split, 419
422 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Detach, 420, 415
423 (t,u) e nn'
Split, 422
As Required:
424 ALL(a):ALL(b):[(a,b) e f'' => (a,b) e nn']
4 Conclusion, 408
425 Set'(f'')
& ALL(a):ALL(b):[(a,b) e f'' => (a,b) e nn']
Join, 402, 424
As Required:
426 f'' e pnn'
Detach, 407, 425
427 ALL(b):[(0,b) e f'' <=> (0,b) e f & ~[0=next(x) & b=y']]
U Spec, 403
428 (0,0') e f'' <=> (0,0') e f & ~[0=next(x) & 0'=y']
U Spec, 427
429 [(0,0') e f'' => (0,0') e f & ~[0=next(x) & 0'=y']]
& [(0,0') e f & ~[0=next(x) & 0'=y'] => (0,0') e f'']
Iff-And, 428
430 (0,0') e f'' => (0,0') e f & ~[0=next(x) & 0'=y']
Split, 429
431 (0,0') e f & ~[0=next(x) & 0'=y'] => (0,0') e f''
Split, 429
Prove: ~[0=next(x) & 0'=y']
Suppose to the contrary...
432 0=next(x) & 0'=y'
Premise
433 0=next(x)
Split, 432
434 0'=y'
Split, 432
435 x e n => ~next(x)=0
U Spec, 5
436 ~next(x)=0
Detach, 435, 370
437 next(x)=0
Sym, 433
438 next(x)=0 & ~next(x)=0
Join, 437, 436
As Required:
439 ~[0=next(x) & 0'=y']
4 Conclusion, 432
440 (0,0') e f & ~[0=next(x) & 0'=y']
Join, 48, 439
As Required:
441 (0,0') e f''
Detach, 431, 440
Prove: ALL(a):ALL(b):[(a,b) e f'' => (next(a),next'(b)) e f'']
Suppose...
442 (t,u) e f''
Premise
443 ALL(b):[(t,b) e f'' <=> (t,b) e f & ~[t=next(x) & b=y']]
U Spec, 403
444 (t,u) e f'' <=> (t,u) e f & ~[t=next(x) & u=y']
U Spec, 443
445 [(t,u) e f'' => (t,u) e f & ~[t=next(x) & u=y']]
& [(t,u) e f & ~[t=next(x) & u=y'] => (t,u) e f'']
Iff-And, 444
446 (t,u) e f'' => (t,u) e f & ~[t=next(x) & u=y']
Split, 445
447 (t,u) e f & ~[t=next(x) & u=y'] => (t,u) e f''
Split, 445
448 (t,u) e f & ~[t=next(x) & u=y']
Detach, 446, 442
449 (t,u) e f
Split, 448
450 ~[t=next(x) & u=y']
Split, 448
451 ALL(b):[(t,b) e f <=> (t,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,b) e c]]
U Spec, 30
452 (t,u) e f <=> (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
U Spec, 451
453 [(t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]]
& [(t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f]
Iff-And, 452
454 (t,u) e f => (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 453
455 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c] => (t,u) e f
Split, 453
456 (t,u) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Detach, 454, 449
457 (t,u) e nn'
Split, 456
458 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (t,u) e c]
Split, 456
459 ALL(c2):[(t,c2) e nn' <=> t e n & c2 e n']
U Spec, 20
460 (t,u) e nn' <=> t e n & u e n'
U Spec, 459
461 [(t,u) e nn' => t e n & u e n']
& [t e n & u e n' => (t,u) e nn']
Iff-And, 460
462 (t,u) e nn' => t e n & u e n'
Split, 461
463 t e n & u e n' => (t,u) e nn'
Split, 461
464 t e n & u e n'
Detach, 462, 457
465 t e n
Split, 464
466 u e n'
Split, 464
467 ALL(b):[(next(t),b) e f'' <=> (next(t),b) e f & ~[next(t)=next(x) & b=y']]
U Spec, 403
468 (next(t),next'(u)) e f'' <=> (next(t),next'(u)) e f & ~[next(t)=next(x) & next'(u)=y']
U Spec, 467
469 [(next(t),next'(u)) e f'' => (next(t),next'(u)) e f & ~[next(t)=next(x) & next'(u)=y']]
& [(next(t),next'(u)) e f & ~[next(t)=next(x) & next'(u)=y'] => (next(t),next'(u)) e f'']
Iff-And, 468
470 (next(t),next'(u)) e f'' => (next(t),next'(u)) e f & ~[next(t)=next(x) & next'(u)=y']
Split, 469
Sufficient: (next(t),next'(u)) e f''
471 (next(t),next'(u)) e f & ~[next(t)=next(x) & next'(u)=y'] => (next(t),next'(u)) e f''
Split, 469
472 ALL(b):[t e n & b e n' => [(t,b) e f => (next(t),next'(b)) e f]]
U Spec, 90
473 t e n & u e n' => [(t,u) e f => (next(t),next'(u)) e f]
U Spec, 472
474 t e n & u e n'
Join, 465, 466
475 (t,u) e f => (next(t),next'(u)) e f
Detach, 473, 474
476 (next(t),next'(u)) e f
Detach, 475, 449
Prove: ~[next(t)=next(x) & next'(u)=y']
Suppose to the contrary...
477 next(t)=next(x) & next'(u)=y'
Premise
478 next(t)=next(x)
Split, 477
479 next'(u)=y'
Split, 477
480 ALL(b):[t e n & b e n => [next(t)=next(b) => t=b]]
U Spec, 4
481 t e n & x e n => [next(t)=next(x) => t=x]
U Spec, 480
482 t e n & x e n
Join, 465, 370
483 next(t)=next(x) => t=x
Detach, 481, 482
484 t=x
Detach, 483, 478
485 (x,y) e f & (x,u) e f => y=u
U Spec, 383
486 (x,y) e f & (t,u) e f => y=u
Substitute, 484, 485
487 (x,y) e f & (t,u) e f
Join, 382, 449
488 y=u
Detach, 486, 487
489 next'(y)=y'
Substitute, 488, 479
490 ~next'(y)=y'
Sym, 387
491 next'(y)=y' & ~next'(y)=y'
Join, 489, 490
492 ~[next(t)=next(x) & next'(u)=y']
4 Conclusion, 477
493 (next(t),next'(u)) e f
& ~[next(t)=next(x) & next'(u)=y']
Join, 476, 492
494 (next(t),next'(u)) e f''
Detach, 471, 493
As Required:
495 ALL(a):ALL(b):[(a,b) e f'' => (next(a),next'(b)) e f'']
4 Conclusion, 442
496 ALL(b):[(next(x),b) e f'' <=> (next(x),b) e f & ~[next(x)=next(x) & b=y']]
U Spec, 403
497 (next(x),y') e f'' <=> (next(x),y') e f & ~[next(x)=next(x) & y'=y']
U Spec, 496
498 [(next(x),y') e f'' => (next(x),y') e f & ~[next(x)=next(x) & y'=y']]
& [(next(x),y') e f & ~[next(x)=next(x) & y'=y'] => (next(x),y') e f'']
Iff-And, 497
499 (next(x),y') e f'' => (next(x),y') e f & ~[next(x)=next(x) & y'=y']
Split, 498
500 (next(x),y') e f & ~[next(x)=next(x) & y'=y'] => (next(x),y') e f''
Split, 498
501 ~[(next(x),y') e f & ~[next(x)=next(x) & y'=y']] => ~(next(x),y') e f''
Contra, 499
502 ~~[~(next(x),y') e f | ~~[next(x)=next(x) & y'=y']] => ~(next(x),y') e f''
DeMorgan, 501
503 ~(next(x),y') e f | ~~[next(x)=next(x) & y'=y'] => ~(next(x),y') e f''
Rem DNeg, 502
504 ~(next(x),y') e f | next(x)=next(x) & y'=y' => ~(next(x),y') e f''
Rem DNeg, 503
505 next(x)=next(x)
Reflex
506 y'=y'
Reflex
507 next(x)=next(x) & y'=y'
Join, 505, 506
508 ~(next(x),y') e f | next(x)=next(x) & y'=y'
Arb Or, 507
509 ~(next(x),y') e f''
Detach, 504, 508
510 f'' e pnn' & (0,0') e f''
Join, 426, 441
511 f'' e pnn' & (0,0') e f''
& ALL(a):ALL(b):[(a,b) e f'' => (next(a),next'(b)) e f'']
Join, 510, 495
512 f'' e pnn' & (0,0') e f''
& ALL(a):ALL(b):[(a,b) e f'' => (next(a),next'(b)) e f'']
& ~(next(x),y') e f''
Join, 511, 509
513 EXIST(c):[c e pnn' & (0,0') e c
& ALL(a):ALL(b):[(a,b) e c => (next(a),next'(b)) e c]
& ~(next(x),y') e c]
E Gen, 512
514 ~(next(x),y') e nn' | EXIST(c):[c e pnn' & (0,0') e c
& ALL(a):ALL(b):[(a,b) e c => (next(a),next'(b)) e c]
& ~(next(x),y') e c]
Arb Or, 513
515 ~(next(x),y') e f
Detach, 399, 514
516 (next(x),y') e f & ~(next(x),y') e f
Join, 386, 515
As Required:
517 ~[(next(x),y') e f & ~y'=next'(y)]
4 Conclusion, 385
518 ~~[(next(x),y') e f => ~~y'=next'(y)]
Imply-And, 517
519 (next(x),y') e f => ~~y'=next'(y)
Rem DNeg, 518
520 (next(x),y') e f => y'=next'(y)
Rem DNeg, 519
As Required:
521 ALL(c):[c e n' => [(next(x),c) e f => c=next'(y)]]
4 Conclusion, 384
Prove: ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]
Suppose...
522 (next(x),y1) e f & (next(x),y2) e f
Premise
523 (next(x),y1) e f
Split, 522
524 (next(x),y2) e f
Split, 522
525 ALL(b):[(next(x),b) e f <=> (next(x),b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),b) e c]]
U Spec, 30
526 (next(x),y1) e f <=> (next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c]
U Spec, 525
527 [(next(x),y1) e f => (next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c]]
& [(next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c] => (next(x),y1) e f]
Iff-And, 526
528 (next(x),y1) e f => (next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c]
Split, 527
529 (next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c] => (next(x),y1) e f
Split, 527
530 (next(x),y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c]
Detach, 528, 523
531 (next(x),y1) e nn'
Split, 530
532 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y1) e c]
Split, 530
533 ALL(c2):[(next(x),c2) e nn' <=> next(x) e n & c2 e n']
U Spec, 20
534 (next(x),y1) e nn' <=> next(x) e n & y1 e n'
U Spec, 533
535 [(next(x),y1) e nn' => next(x) e n & y1 e n']
& [next(x) e n & y1 e n' => (next(x),y1) e nn']
Iff-And, 534
536 (next(x),y1) e nn' => next(x) e n & y1 e n'
Split, 535
537 next(x) e n & y1 e n' => (next(x),y1) e nn'
Split, 535
538 next(x) e n & y1 e n'
Detach, 536, 531
539 next(x) e n
Split, 538
540 y1 e n'
Split, 538
541 (next(x),y2) e f <=> (next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c]
U Spec, 525
542 [(next(x),y2) e f => (next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c]]
& [(next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c] => (next(x),y2) e f]
Iff-And, 541
543 (next(x),y2) e f => (next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c]
Split, 542
544 (next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c] => (next(x),y2) e f
Split, 542
545 (next(x),y2) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c]
Detach, 543, 524
546 (next(x),y2) e nn'
Split, 545
547 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),y2) e c]
Split, 545
548 (next(x),y2) e nn' <=> next(x) e n & y2 e n'
U Spec, 533
549 [(next(x),y2) e nn' => next(x) e n & y2 e n']
& [next(x) e n & y2 e n' => (next(x),y2) e nn']
Iff-And, 548
550 (next(x),y2) e nn' => next(x) e n & y2 e n'
Split, 549
551 next(x) e n & y2 e n' => (next(x),y2) e nn'
Split, 549
552 next(x) e n & y2 e n'
Detach, 550, 546
553 next(x) e n
Split, 552
554 y2 e n'
Split, 552
555 y1 e n' => [(next(x),y1) e f => y1=next'(y)]
U Spec, 521
556 (next(x),y1) e f => y1=next'(y)
Detach, 555, 540
557 y1=next'(y)
Detach, 556, 523
558 y2 e n' => [(next(x),y2) e f => y2=next'(y)]
U Spec, 521
559 (next(x),y2) e f => y2=next'(y)
Detach, 558, 554
560 y2=next'(y)
Detach, 559, 524
561 y1=y2
Substitute, 560, 557
As Required:
562 ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]
4 Conclusion, 522
563 next(x) e n
& ALL(b1):ALL(b2):[(next(x),b1) e f & (next(x),b2) e f => b1=b2]
Join, 377, 562
564 next(x) e p2
Detach, 375, 563
As Required:
565 ALL(a):[a e p2 => next(a) e p2]
4 Conclusion, 364
566 0 e p2 & ALL(a):[a e p2 => next(a) e p2]
Join, 363, 565
As Required:
567 ALL(b):[b e n => b e p2]
Detach, 316, 566
Prove: ALL(a):[a e n => ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
Suppose...
568 x e n
Premise
569 x e n => x e p2
U Spec, 567
570 x e p2
Detach, 569, 568
571 x e p2 <=> x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
U Spec, 305
572 [x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]]
& [x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2]
Iff-And, 571
573 x e p2 => x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Split, 572
574 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2] => x e p2
Split, 572
575 x e n & ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Detach, 573, 570
576 x e n
Split, 575
577 ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Split, 575
As Required:
578 ALL(a):[a e n
=> ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]]
4 Conclusion, 568
Prove: ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Suppose...
579 (x,y1) e f & (x,y2) e f
Premise
580 (x,y1) e f
Split, 579
581 (x,y2) e f
Split, 579
Sufficient: ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
582 x e n
=> ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
U Spec, 578
583 ALL(b):[(x,b) e f <=> (x,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,b) e c]]
U Spec, 30
584 (x,y1) e f <=> (x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c]
U Spec, 583
585 [(x,y1) e f => (x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c]]
& [(x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c] => (x,y1) e f]
Iff-And, 584
586 (x,y1) e f => (x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c]
Split, 585
587 (x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c] => (x,y1) e f
Split, 585
588 (x,y1) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c]
Detach, 586, 580
589 (x,y1) e nn'
Split, 588
590 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y1) e c]
Split, 588
591 ALL(c2):[(x,c2) e nn' <=> x e n & c2 e n']
U Spec, 20
592 (x,y1) e nn' <=> x e n & y1 e n'
U Spec, 591
593 [(x,y1) e nn' => x e n & y1 e n']
& [x e n & y1 e n' => (x,y1) e nn']
Iff-And, 592
594 (x,y1) e nn' => x e n & y1 e n'
Split, 593
595 x e n & y1 e n' => (x,y1) e nn'
Split, 593
596 x e n & y1 e n'
Detach, 594, 589
597 x e n
Split, 596
598 y1 e n'
Split, 596
599 ALL(b1):ALL(b2):[(x,b1) e f & (x,b2) e f => b1=b2]
Detach, 582, 597
600 ALL(b2):[(x,y1) e f & (x,b2) e f => y1=b2]
U Spec, 599
601 (x,y1) e f & (x,y2) e f => y1=y2
U Spec, 600
602 y1=y2
Detach, 601, 579
As Required: Functionality, Part 3
603 ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
4 Conclusion, 579
604 ALL(a):ALL(b):[(a,b) e f => a e n & b e n']
& ALL(a):[a e n => EXIST(b):[b e n' & (a,b) e f]]
Join, 110, 175
605 ALL(a):ALL(b):[(a,b) e f => a e n & b e n']
& ALL(a):[a e n => EXIST(b):[b e n' & (a,b) e f]]
& ALL(a):ALL(b1):ALL(b2):[(a,b1) e f & (a,b2) e f => b1=b2]
Join, 604, 603
f is a function
606 ALL(c):ALL(d):[d=f(c) <=> (c,d) e f]
Detach, 94, 605
Prove: ALL(a):[a e n => f(a) e n']
Suppose...
607 x e n
Premise
608 x e n => EXIST(b):[b e n' & (x,b) e f]
U Spec, 175
609 EXIST(b):[b e n' & (x,b) e f]
Detach, 608, 607
610 y e n' & (x,y) e f
E Spec, 609
611 y e n'
Split, 610
612 (x,y) e f
Split, 610
613 ALL(d):[d=f(x) <=> (x,d) e f]
U Spec, 606
614 y=f(x) <=> (x,y) e f
U Spec, 613
615 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]
Iff-And, 614
616 y=f(x) => (x,y) e f
Split, 615
617 (x,y) e f => y=f(x)
Split, 615
618 y=f(x)
Detach, 617, 612
619 f(x) e n'
Substitute, 618, 611
As Required:
620 ALL(a):[a e n => f(a) e n']
4 Conclusion, 607
Prove: f(0)=0'
621 ALL(d):[d=f(0) <=> (0,d) e f]
U Spec, 606
622 0'=f(0) <=> (0,0') e f
U Spec, 621
623 [0'=f(0) => (0,0') e f] & [(0,0') e f => 0'=f(0)]
Iff-And, 622
624 0'=f(0) => (0,0') e f
Split, 623
625 (0,0') e f => 0'=f(0)
Split, 623
626 0'=f(0)
Detach, 625, 48
As Required:
627 f(0)=0'
Sym, 626
Prove: ALL(a):[a e n => f(next(a))=next'(f(a))]
Suppose...
628 x e n
Premise
629 x e n => EXIST(b):[b e n' & (x,b) e f]
U Spec, 175
630 EXIST(b):[b e n' & (x,b) e f]
Detach, 629, 628
631 y e n' & (x,y) e f
E Spec, 630
Define: y
632 y e n'
Split, 631
633 (x,y) e f
Split, 631
634 ALL(b):[(x,b) e f <=> (x,b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,b) e c]]
U Spec, 30
635 (x,y) e f <=> (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
U Spec, 634
636 [(x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]]
& [(x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f]
Iff-And, 635
637 (x,y) e f => (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 636
638 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c] => (x,y) e f
Split, 636
639 (x,y) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Detach, 637, 633
640 (x,y) e nn'
Split, 639
641 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (x,y) e c]
Split, 639
642 ALL(d):[d=f(x) <=> (x,d) e f]
U Spec, 606
643 y=f(x) <=> (x,y) e f
U Spec, 642
644 [y=f(x) => (x,y) e f] & [(x,y) e f => y=f(x)]
Iff-And, 643
645 y=f(x) => (x,y) e f
Split, 644
646 (x,y) e f => y=f(x)
Split, 644
647 y=f(x)
Detach, 646, 633
648 ALL(b):[(next(x),b) e f <=> (next(x),b) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),b) e c]]
U Spec, 30
649 (next(x),next'(y)) e f <=> (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
U Spec, 648
650 [(next(x),next'(y)) e f => (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]]
& [(next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c] => (next(x),next'(y)) e f]
Iff-And, 649
651 (next(x),next'(y)) e f => (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Split, 650
Sufficient: (next(x),next'(y)) e f
652 (next(x),next'(y)) e nn' & ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c] => (next(x),next'(y)) e f
Split, 650
653 ALL(c2):[(next(x),c2) e nn' <=> next(x) e n & c2 e n']
U Spec, 20
654 (next(x),next'(y)) e nn' <=> next(x) e n & next'(y) e n'
U Spec, 653
655 [(next(x),next'(y)) e nn' => next(x) e n & next'(y) e n']
& [next(x) e n & next'(y) e n' => (next(x),next'(y)) e nn']
Iff-And, 654
656 (next(x),next'(y)) e nn' => next(x) e n & next'(y) e n'
Split, 655
657 next(x) e n & next'(y) e n' => (next(x),next'(y)) e nn'
Split, 655
658 x e n => next(x) e n
U Spec, 3
659 next(x) e n
Detach, 658, 628
660 y e n' => next'(y) e n'
U Spec, 9
661 next'(y) e n'
Detach, 660, 632
662 next(x) e n & next'(y) e n'
Join, 659, 661
As Required:
663 (next(x),next'(y)) e nn'
Detach, 657, 662
Prove: ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Suppose...
664 q e pnn'
& (0,0') e q
& ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
Premise
665 q e pnn'
Split, 664
666 (0,0') e q
Split, 664
667 ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
Split, 664
668 q e pnn'
& (0,0') e q
& ALL(d):ALL(e):[(d,e) e q => (next(d),next'(e)) e q]
=> (x,y) e q
U Spec, 641
669 (x,y) e q
Detach, 668, 664
670 ALL(e):[(x,e) e q => (next(x),next'(e)) e q]
U Spec, 667
671 (x,y) e q => (next(x),next'(y)) e q
U Spec, 670
672 (next(x),next'(y)) e q
Detach, 671, 669
As Required:
673 ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
4 Conclusion, 664
674 (next(x),next'(y)) e nn'
& ALL(c):[c e pnn'
& (0,0') e c
& ALL(d):ALL(e):[(d,e) e c => (next(d),next'(e)) e c]
=> (next(x),next'(y)) e c]
Join, 663, 673
675 (next(x),next'(y)) e f
Detach, 652, 674
676 ALL(d):[d=f(next(x)) <=> (next(x),d) e f]
U Spec, 606
677 next'(y)=f(next(x)) <=> (next(x),next'(y)) e f
U Spec, 676
678 [next'(y)=f(next(x)) => (next(x),next'(y)) e f]
& [(next(x),next'(y)) e f => next'(y)=f(next(x))]
Iff-And, 677
679 next'(y)=f(next(x)) => (next(x),next'(y)) e f
Split, 678
680 (next(x),next'(y)) e f => next'(y)=f(next(x))
Split, 678
681 next'(y)=f(next(x))
Detach, 680, 675
682 next'(f(x))=f(next(x))
Substitute, 647, 681
683 f(next(x))=next'(f(x))
Sym, 682
As Required:
684 ALL(a):[a e n => f(next(a))=next'(f(a))]
4 Conclusion, 628
685 ALL(a):[a e n => f(a) e n'] & f(0)=0'
Join, 620, 627
686 ALL(a):[a e n => f(a) e n'] & f(0)=0'
& ALL(a):[a e n => f(next(a))=next'(f(a))]
Join, 685, 684
As Required:
687 EXIST(f):[ALL(a):[a e n => f(a) e n'] & f(0)=0'
& ALL(a):[a e n => f(next(a))=next'(f(a))]]
E Gen, 686