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