THEOREM
-------
Given sets right and left, functions f and g, and element 0 such that
1. f is an injective function defined on right
2. g is an injective function defined on left
3. 0 is the only element common to both right and left
4. 0 has no pre-image in right under f
5. 0 has no pre-image in left under g
Then there exists sets z, zright and zleft, element 0, and functions next and next' such that
1. z is the union of zright and zleft
2. 0 is the only element common to zright and zleft
3. next and next' are functions defined on z
4. next' is the inverse of next
5. next is closed on zright
6. next' is closed on zleft
7. 0 has no pre-image in zright under next
8. 0 has no pre-image in zleft under next'
9. For all subsets a of z, if
(a) 0 e a
(b) if b e a, then next(b) e a
(c) if b e a, then next'(b) e a
then z is a subset of a
where
z is the set of integers (or an "integer-like" set)
zright is the set of non-negative integers, a subset of right
zleft is the set of non-positive integers, a subset of left
next(x) = f(x) for x in zright
next'(x) = g(x) for x in zleft
This proof was written with the aid of the author's DC Proof 2.0 software available at
Previous Results
****************
Natural-number-like structures embedded in other sets
1 ALL(s):ALL(f):[Set(s)
& ALL(b):[b e s => f(b) e s]
& ALL(b):ALL(c):[b e s & c e s => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e s & ALL(b):[b e s => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e s] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e s] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]]
Axiom
All elements of n but s1 have a predeccesor in n
2 ALL(n):ALL(s1):ALL(f):[Set(n)
& s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
=> ALL(a):[a e n => [~a=s1 => EXIST(b):[b e n & f(b)=a]]]]
Axiom
Inverse functions
3 ALL(x):ALL(y):ALL(f):[Set(x) & Set(y)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]
& ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e x]
& ALL(a):ALL(b):[a e x & b e y => [f'(b)=a <=> f(a)=b]]]]
Axiom
Suppose...
4 Set(right)
& ALL(a):[a e right => f(a) e right]
& ALL(a):ALL(b):[a e right & b e right => [f(a)=f(b) => a=b]]
& Set(left)
& ALL(a):[a e left => g(a) e left]
& ALL(a):ALL(b):[a e left & b e left => [g(a)=g(b) => a=b]]
& EXIST(0):[ALL(a):[a e right & a e left <=> a=0]
& ALL(a):[a e right => ~f(a)=0]
& ALL(a):[a e left => ~g(a)=0]]
Premise
Splitting this premise into its component parts...
Define: f
*********
f is an injective function on the set right
5 Set(right)
Split, 4
6 ALL(a):[a e right => f(a) e right]
Split, 4
7 ALL(a):ALL(b):[a e right & b e right => [f(a)=f(b) => a=b]]
Split, 4
Define: g
*********
g is an injective function on the set left
8 Set(left)
Split, 4
9 ALL(a):[a e left => g(a) e left]
Split, 4
10 ALL(a):ALL(b):[a e left & b e left => [g(a)=g(b) => a=b]]
Split, 4
11 EXIST(0):[ALL(a):[a e right & a e left <=> a=0]
& ALL(a):[a e right => ~f(a)=0]
& ALL(a):[a e left => ~g(a)=0]]
Split, 4
12 ALL(a):[a e right & a e left <=> a=0]
& ALL(a):[a e right => ~f(a)=0]
& ALL(a):[a e left => ~g(a)=0]
E Spec, 11
Define: 0 (in right and left)
*********
13 ALL(a):[a e right & a e left <=> a=0]
Split, 12
14 ALL(a):[a e right => ~f(a)=0]
Split, 12
15 ALL(a):[a e left => ~g(a)=0]
Split, 12
Some preliminary lemmas...
16 0 e right & 0 e left <=> 0=0
U Spec, 13
17 [0 e right & 0 e left => 0=0]
& [0=0 => 0 e right & 0 e left]
Iff-And, 16
18 0 e right & 0 e left => 0=0
Split, 17
19 0=0 => 0 e right & 0 e left
Split, 17
20 0=0
Reflex
21 0 e right & 0 e left
Detach, 19, 20
Lemma 1
22 0 e right
Split, 21
Lemma 2
23 0 e left
Split, 21
Apply previous result for right
24 ALL(f):[Set(right)
& ALL(b):[b e right => f(b) e right]
& ALL(b):ALL(c):[b e right & c e right => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e right & ALL(b):[b e right => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e right] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]]
U Spec, 1
25 Set(right)
& ALL(b):[b e right => f(b) e right]
& ALL(b):ALL(c):[b e right & c e right => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e right & ALL(b):[b e right => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e right] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
U Spec, 24
26 Set(right) & ALL(a):[a e right => f(a) e right]
Join, 5, 6
27 Set(right) & ALL(a):[a e right => f(a) e right]
& ALL(a):ALL(b):[a e right & b e right => [f(a)=f(b) => a=b]]
Join, 26, 7
28 ALL(s1):[s1 e right & ALL(b):[b e right => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e right] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
Detach, 25, 27
29 0 e right & ALL(b):[b e right => ~f(b)=0]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e right] & 0 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & 0 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
U Spec, 28
30 0 e right & ALL(a):[a e right => ~f(a)=0]
Join, 22, 14
31 EXIST(n):[Set(n) & ALL(b):[b e n => b e right] & 0 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & 0 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
Detach, 29, 30
32 Set(zright) & ALL(b):[b e zright => b e right] & 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & 0 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=zright]
E Spec, 31
Define: zright (non-negative integers)
**************
33 Set(zright)
Split, 32
zright is a subset of right
34 ALL(b):[b e zright => b e right]
Split, 32
35 0 e zright
Split, 32
f is closed on zright
36 ALL(b):[b e zright => f(b) e zright]
Split, 32
f is injective on zright
37 ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
Split, 32
0 has no pre-image in zright under f
38 ALL(b):[b e zright => ~f(b)=0]
Split, 32
Induction defined on zright
39 ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
Split, 32
zright is unique (not used here)
40 ALL(n'):[Set(n') & ALL(b):[b e n' => b e right] & 0 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=zright]
Split, 32
Apply previous result for left
41 ALL(f):[Set(left)
& ALL(b):[b e left => f(b) e left]
& ALL(b):ALL(c):[b e left & c e left => [f(b)=f(c) => b=c]]
=> ALL(s1):[s1 e left & ALL(b):[b e left => ~f(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e left] & s1 e n
& ALL(b):[b e n => f(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & s1 e n'
& ALL(b):[b e n' => f(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [f(b)=f(c) => b=c]]
& ALL(b):[b e n' => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]]
U Spec, 1
42 Set(left)
& ALL(b):[b e left => g(b) e left]
& ALL(b):ALL(c):[b e left & c e left => [g(b)=g(c) => b=c]]
=> ALL(s1):[s1 e left & ALL(b):[b e left => ~g(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e left] & s1 e n
& ALL(b):[b e n => g(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n => ~g(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & s1 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
U Spec, 41
43 Set(left) & ALL(a):[a e left => g(a) e left]
Join, 8, 9
44 Set(left) & ALL(a):[a e left => g(a) e left]
& ALL(a):ALL(b):[a e left & b e left => [g(a)=g(b) => a=b]]
Join, 43, 10
45 ALL(s1):[s1 e left & ALL(b):[b e left => ~g(b)=s1]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e left] & s1 e n
& ALL(b):[b e n => g(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n => ~g(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& s1 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & s1 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& s1 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]]
Detach, 42, 44
46 0 e left & ALL(b):[b e left => ~g(b)=0]
=> EXIST(n):[Set(n) & ALL(b):[b e n => b e left] & 0 e n
& ALL(b):[b e n => g(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & 0 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
U Spec, 45
47 0 e left & ALL(a):[a e left => ~g(a)=0]
Join, 23, 15
48 EXIST(n):[Set(n) & ALL(b):[b e n => b e left] & 0 e n
& ALL(b):[b e n => g(b) e n]
& ALL(b):ALL(c):[b e n & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & 0 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e n => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=n]]
Detach, 46, 47
49 Set(zleft) & ALL(b):[b e zleft => b e left] & 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e zleft => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e zleft => c e b]]
& ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & 0 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=zleft]
E Spec, 48
Define: zleft (non-positive integers)
*************
50 Set(zleft)
Split, 49
zleft is a subset of left
51 ALL(b):[b e zleft => b e left]
Split, 49
52 0 e zleft
Split, 49
g is closed on zleft
53 ALL(b):[b e zleft => g(b) e zleft]
Split, 49
g is inective on zleft
54 ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
Split, 49
g has no pre-image of 0 in zleft under g
55 ALL(b):[b e zleft => ~g(b)=0]
Split, 49
Induction defined on zleft
56 ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e zleft => c e b]]
Split, 49
zleft unique (not used here)
57 ALL(n'):[Set(n') & ALL(b):[b e n' => b e left] & 0 e n'
& ALL(b):[b e n' => g(b) e n']
& ALL(b):ALL(c):[b e n' & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e n' => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e n']
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e n' => c e b]]
=> n'=zleft]
Split, 49
Construct union of zright and zleft
Apply Pairwise Union Axiom
58 ALL(a):ALL(b):[Set(a) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d e c <=> d e a | d e b]]]
Pw Union
59 ALL(b):[Set(zright) & Set(b) => EXIST(c):[Set(c) & ALL(d):[d e c <=> d e zright | d e b]]]
U Spec, 58
60 Set(zright) & Set(zleft) => EXIST(c):[Set(c) & ALL(d):[d e c <=> d e zright | d e zleft]]
U Spec, 59
61 Set(zright) & Set(zleft)
Join, 33, 50
62 EXIST(c):[Set(c) & ALL(d):[d e c <=> d e zright | d e zleft]]
Detach, 60, 61
63 Set(z) & ALL(d):[d e z <=> d e zright | d e zleft]
E Spec, 62
Define: z (the set of integers)
*********
64 Set(z)
Split, 63
z is the union of zright and zleft
65 ALL(d):[d e z <=> d e zright | d e zleft]
Split, 63
Preliminary lemmas...
66 0 e z <=> 0 e zright | 0 e zleft
U Spec, 65
67 [0 e z => 0 e zright | 0 e zleft]
& [0 e zright | 0 e zleft => 0 e z]
Iff-And, 66
68 0 e z => 0 e zright | 0 e zleft
Split, 67
69 0 e zright | 0 e zleft => 0 e z
Split, 67
70 0 e zright | 0 e zleft
Arb Or, 35
Lemma 3
71 0 e z
Detach, 69, 70
Suppose...
72 x e zright & x e zleft
Premise
73 x e zright
Split, 72
74 x e zleft
Split, 72
75 x e zright => x e right
U Spec, 34
76 x e right
Detach, 75, 73
77 x e zleft => x e left
U Spec, 51
78 x e left
Detach, 77, 74
79 x e right & x e left <=> x=0
U Spec, 13
80 [x e right & x e left => x=0]
& [x=0 => x e right & x e left]
Iff-And, 79
81 x e right & x e left => x=0
Split, 80
82 x=0 => x e right & x e left
Split, 80
83 x e right & x e left
Join, 76, 78
84 x=0
Detach, 81, 83
85 ALL(a):[a e zright & a e zleft => a=0]
4 Conclusion, 72
86 x=0
Premise
87 x e zright
Substitute, 86, 35
88 x e zleft
Substitute, 86, 52
89 x e zright & x e zleft
Join, 87, 88
90 ALL(a):[a=0 => a e zright & a e zleft]
4 Conclusion, 86
91 ALL(a):[[a e zright & a e zleft => a=0] & [a=0 => a e zright & a e zleft]]
Join, 85, 90
Lemma 4
0 is common to zright and zleft
92 ALL(a):[a e zright & a e zleft <=> a=0]
Iff-And, 91
Prove: ALL(a):[a e z => [~a e zright => a e zleft & ~a=0]]
Suppose...
93 x e z
Premise
Prove: ~x e zright => x e zleft & ~x=0
Suppose...
94 ~x e zright
Premise
95 x e z <=> x e zright | x e zleft
U Spec, 65
96 [x e z => x e zright | x e zleft]
& [x e zright | x e zleft => x e z]
Iff-And, 95
97 x e z => x e zright | x e zleft
Split, 96
98 x e zright | x e zleft => x e z
Split, 96
99 x e zright | x e zleft
Detach, 97, 93
100 ~x e zright => x e zleft
Imply-Or, 99
101 x e zleft
Detach, 100, 94
102 x=0
Premise
103 ~0 e zright
Substitute, 102, 94
104 0 e zright & ~0 e zright
Join, 35, 103
105 ~x=0
4 Conclusion, 102
106 x e zleft & ~x=0
Join, 101, 105
As Required:
107 ~x e zright => x e zleft & ~x=0
4 Conclusion, 94
Lemma 5
Not non-negative
108 ALL(a):[a e z => [~a e zright => a e zleft & ~a=0]]
4 Conclusion, 93
Prove: ALL(a):[a e zleft & ~a=0 => EXIST(b):[b e zleft & g(b)=a]]
Suppose...
109 x e zleft & ~x=0
Premise
110 x e zleft
Split, 109
111 ~x=0
Split, 109
112 ALL(s1):ALL(f):[Set(zleft)
& s1 e zleft
& ALL(b):[b e zleft => f(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [f(b)=f(c) => b=c]]
& ALL(b):[b e zleft => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zleft => c e b]]
=> ALL(a):[a e zleft => [~a=s1 => EXIST(b):[b e zleft & f(b)=a]]]]
U Spec, 2
113 ALL(f):[Set(zleft)
& 0 e zleft
& ALL(b):[b e zleft => f(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [f(b)=f(c) => b=c]]
& ALL(b):[b e zleft => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zleft => c e b]]
=> ALL(a):[a e zleft => [~a=0 => EXIST(b):[b e zleft & f(b)=a]]]]
U Spec, 112
114 Set(zleft)
& 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e zleft => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e zleft => c e b]]
=> ALL(a):[a e zleft => [~a=0 => EXIST(b):[b e zleft & g(b)=a]]]
U Spec, 113
115 Set(zleft) & 0 e zleft
Join, 50, 52
116 Set(zleft) & 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
Join, 115, 53
117 Set(zleft) & 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
Join, 116, 54
118 Set(zleft) & 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e zleft => ~g(b)=0]
Join, 117, 55
119 Set(zleft) & 0 e zleft
& ALL(b):[b e zleft => g(b) e zleft]
& ALL(b):ALL(c):[b e zleft & c e zleft => [g(b)=g(c) => b=c]]
& ALL(b):[b e zleft => ~g(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zleft]
& 0 e b
& ALL(c):[c e b => g(c) e b]
=> ALL(c):[c e zleft => c e b]]
Join, 118, 56
120 ALL(a):[a e zleft => [~a=0 => EXIST(b):[b e zleft & g(b)=a]]]
Detach, 114, 119
121 x e zleft => [~x=0 => EXIST(b):[b e zleft & g(b)=x]]
U Spec, 120
122 ~x=0 => EXIST(b):[b e zleft & g(b)=x]
Detach, 121, 110
123 EXIST(b):[b e zleft & g(b)=x]
Detach, 122, 111
Lemma 6
Existence of predecessors for negative integers
124 ALL(a):[a e zleft & ~a=0 => EXIST(b):[b e zleft & g(b)=a]]
4 Conclusion, 109
Apply Cartesian Product Axiom
125 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
126 ALL(a2):[Set(z) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e z & c2 e a2]]]
U Spec, 125
127 Set(z) & Set(z) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e z & c2 e z]]
U Spec, 126
128 Set(z) & Set(z)
Join, 64, 64
129 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e z & c2 e z]]
Detach, 127, 128
130 Set'(z2) & ALL(c1):ALL(c2):[(c1,c2) e z2 <=> c1 e z & c2 e z]
E Spec, 129
Define: z2 (the set of ordered pairs of integers)
**********
131 Set'(z2)
Split, 130
132 ALL(c1):ALL(c2):[(c1,c2) e z2 <=> c1 e z & c2 e z]
Split, 130
Apply Subset Axiom
133 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e z2 & [a e zright & b e zright & f(a)=b | ~a e zright & b e zleft & g(b)=a]]]
Subset, 131
134 Set'(next) & ALL(a):ALL(b):[(a,b) e next <=> (a,b) e z2 & [a e zright & b e zright & f(a)=b | ~a e zright & b e zleft & g(b)=a]]
E Spec, 133
Define: next
************
135 Set'(next)
Split, 134
136 ALL(a):ALL(b):[(a,b) e next <=> (a,b) e z2 & [a e zright & b e zright & f(a)=b | ~a e zright & b e zleft & g(b)=a]]
Split, 134
Apply Function Axiom (for 1 variable)
137 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
138 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e next => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e next]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
=> ALL(c):ALL(d):[d=next(c) <=> (c,d) e next]]
U Spec, 137
139 ALL(b):[ALL(c):ALL(d):[(c,d) e next => c e z & d e b]
& ALL(c):[c e z => EXIST(d):[d e b & (c,d) e next]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
=> ALL(c):ALL(d):[d=next(c) <=> (c,d) e next]]
U Spec, 138
Sufficient: For functionality of next
140 ALL(c):ALL(d):[(c,d) e next => c e z & d e z]
& ALL(c):[c e z => EXIST(d):[d e z & (c,d) e next]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
=> ALL(c):ALL(d):[d=next(c) <=> (c,d) e next]
U Spec, 139
Suppose...
141 (x,y) e next
Premise
Apply definition of next
142 ALL(b):[(x,b) e next <=> (x,b) e z2 & [x e zright & b e zright & f(x)=b | ~x e zright & b e zleft & g(b)=x]]
U Spec, 136
143 (x,y) e next <=> (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
U Spec, 142
144 [(x,y) e next => (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]]
& [(x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x] => (x,y) e next]
Iff-And, 143
145 (x,y) e next => (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
Split, 144
146 (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x] => (x,y) e next
Split, 144
147 (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
Detach, 145, 141
148 (x,y) e z2
Split, 147
149 ALL(c2):[(x,c2) e z2 <=> x e z & c2 e z]
U Spec, 132
150 (x,y) e z2 <=> x e z & y e z
U Spec, 149
151 [(x,y) e z2 => x e z & y e z]
& [x e z & y e z => (x,y) e z2]
Iff-And, 150
152 (x,y) e z2 => x e z & y e z
Split, 151
153 x e z & y e z => (x,y) e z2
Split, 151
154 x e z & y e z
Detach, 152, 148
Functionality of next, Part 1
155 ALL(c):ALL(d):[(c,d) e next => c e z & d e z]
4 Conclusion, 141
Prove: ALL(c):[c e z => EXIST(d):[d e z & (c,d) e next]]
Suppose...
156 x e z
Premise
Two cases to consider:
157 x e zright | ~x e zright
Or Not
Case 1
Prove: x e zright => EXIST(d):[d e z & (x,d) e next]
Suppose...
158 x e zright
Premise
159 ALL(b):[(x,b) e next <=> (x,b) e z2 & [x e zright & b e zright & f(x)=b | ~x e zright & b e zleft & g(b)=x]]
U Spec, 136
160 (x,f(x)) e next <=> (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
U Spec, 159
161 [(x,f(x)) e next => (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]]
& [(x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x] => (x,f(x)) e next]
Iff-And, 160
162 (x,f(x)) e next => (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
Split, 161
Sufficient: For (x,f(x)) e next
163 (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x] => (x,f(x)) e next
Split, 161
Apply definition of z2
164 ALL(c2):[(x,c2) e z2 <=> x e z & c2 e z]
U Spec, 132
165 (x,f(x)) e z2 <=> x e z & f(x) e z
U Spec, 164
166 [(x,f(x)) e z2 => x e z & f(x) e z]
& [x e z & f(x) e z => (x,f(x)) e z2]
Iff-And, 165
167 (x,f(x)) e z2 => x e z & f(x) e z
Split, 166
168 x e z & f(x) e z => (x,f(x)) e z2
Split, 166
169 x e zright => f(x) e zright
U Spec, 36
170 f(x) e zright
Detach, 169, 158
171 f(x) e z <=> f(x) e zright | f(x) e zleft
U Spec, 65
172 [f(x) e z => f(x) e zright | f(x) e zleft]
& [f(x) e zright | f(x) e zleft => f(x) e z]
Iff-And, 171
173 f(x) e z => f(x) e zright | f(x) e zleft
Split, 172
174 f(x) e zright | f(x) e zleft => f(x) e z
Split, 172
175 f(x) e zright | f(x) e zleft
Arb Or, 170
176 f(x) e z
Detach, 174, 175
177 x e z & f(x) e z
Join, 156, 176
178 (x,f(x)) e z2
Detach, 168, 177
179 f(x)=f(x)
Reflex
180 x e zright & f(x) e zright
Join, 158, 170
181 x e zright & f(x) e zright & f(x)=f(x)
Join, 180, 179
182 x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x
Arb Or, 181
183 (x,f(x)) e z2
& [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
Join, 178, 182
184 (x,f(x)) e next
Detach, 163, 183
185 f(x) e z & (x,f(x)) e next
Join, 176, 184
186 EXIST(d):[d e z & (x,d) e next]
E Gen, 185
As Required:
187 x e zright => EXIST(d):[d e z & (x,d) e next]
4 Conclusion, 158
Prove: ~x e zright => EXIST(d):[d e z & (x,d) e next]
Suppose...
188 ~x e zright
Premise
189 x e z => [~x e zright => x e zleft & ~x=0]
U Spec, 108
190 ~x e zright => x e zleft & ~x=0
Detach, 189, 156
191 x e zleft & ~x=0
Detach, 190, 188
192 x e zleft & ~x=0 => EXIST(b):[b e zleft & g(b)=x]
U Spec, 124
193 EXIST(b):[b e zleft & g(b)=x]
Detach, 192, 191
194 y e zleft & g(y)=x
E Spec, 193
195 y e zleft
Split, 194
196 g(y)=x
Split, 194
197 ALL(b):[(x,b) e next <=> (x,b) e z2 & [x e zright & b e zright & f(x)=b | ~x e zright & b e zleft & g(b)=x]]
U Spec, 136
198 (x,y) e next <=> (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
U Spec, 197
199 [(x,y) e next => (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]]
& [(x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x] => (x,y) e next]
Iff-And, 198
200 (x,y) e next => (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
Split, 199
Sufficient: For (x,y) e next
201 (x,y) e z2 & [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x] => (x,y) e next
Split, 199
202 ALL(c2):[(x,c2) e z2 <=> x e z & c2 e z]
U Spec, 132
203 (x,y) e z2 <=> x e z & y e z
U Spec, 202
204 [(x,y) e z2 => x e z & y e z]
& [x e z & y e z => (x,y) e z2]
Iff-And, 203
205 (x,y) e z2 => x e z & y e z
Split, 204
206 x e z & y e z => (x,y) e z2
Split, 204
207 y e z <=> y e zright | y e zleft
U Spec, 65
208 [y e z => y e zright | y e zleft]
& [y e zright | y e zleft => y e z]
Iff-And, 207
209 y e z => y e zright | y e zleft
Split, 208
210 y e zright | y e zleft => y e z
Split, 208
211 y e zright | y e zleft
Arb Or, 195
212 y e z
Detach, 210, 211
213 x e z & y e z
Join, 156, 212
214 (x,y) e z2
Detach, 206, 213
215 ~x e zright & y e zleft
Join, 188, 195
216 ~x e zright & y e zleft & g(y)=x
Join, 215, 196
217 x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x
Arb Or, 216
218 (x,y) e z2
& [x e zright & y e zright & f(x)=y | ~x e zright & y e zleft & g(y)=x]
Join, 214, 217
219 (x,y) e next
Detach, 201, 218
220 y e z & (x,y) e next
Join, 212, 219
221 EXIST(d):[d e z & (x,d) e next]
E Gen, 220
As Required:
222 ~x e zright => EXIST(d):[d e z & (x,d) e next]
4 Conclusion, 188
223 [x e zright => EXIST(d):[d e z & (x,d) e next]]
& [~x e zright => EXIST(d):[d e z & (x,d) e next]]
Join, 187, 222
224 EXIST(d):[d e z & (x,d) e next]
Cases, 157, 223
Functionality of next, Part 2
225 ALL(c):[c e z => EXIST(d):[d e z & (c,d) e next]]
4 Conclusion, 156
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
Suppose...
226 (x,y1) e next & (x,y2) e next
Premise
227 (x,y1) e next
Split, 226
228 (x,y2) e next
Split, 226
229 ALL(b):[(x,b) e next <=> (x,b) e z2 & [x e zright & b e zright & f(x)=b | ~x e zright & b e zleft & g(b)=x]]
U Spec, 136
230 (x,y1) e next <=> (x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x]
U Spec, 229
231 [(x,y1) e next => (x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x]]
& [(x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x] => (x,y1) e next]
Iff-And, 230
232 (x,y1) e next => (x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x]
Split, 231
233 (x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x] => (x,y1) e next
Split, 231
234 (x,y1) e z2 & [x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x]
Detach, 232, 227
235 (x,y1) e z2
Split, 234
236 x e zright & y1 e zright & f(x)=y1 | ~x e zright & y1 e zleft & g(y1)=x
Split, 234
237 (x,y2) e next <=> (x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x]
U Spec, 229
238 [(x,y2) e next => (x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x]]
& [(x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x] => (x,y2) e next]
Iff-And, 237
239 (x,y2) e next => (x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x]
Split, 238
240 (x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x] => (x,y2) e next
Split, 238
241 (x,y2) e z2 & [x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x]
Detach, 239, 228
242 (x,y2) e z2
Split, 241
243 x e zright & y2 e zright & f(x)=y2 | ~x e zright & y2 e zleft & g(y2)=x
Split, 241
244 ALL(c2):[(x,c2) e z2 <=> x e z & c2 e z]
U Spec, 132
245 (x,y1) e z2 <=> x e z & y1 e z
U Spec, 244
246 [(x,y1) e z2 => x e z & y1 e z]
& [x e z & y1 e z => (x,y1) e z2]
Iff-And, 245
247 (x,y1) e z2 => x e z & y1 e z
Split, 246
248 x e z & y1 e z => (x,y1) e z2
Split, 246
249 x e z & y1 e z
Detach, 247, 235
250 x e z
Split, 249
251 y1 e z
Split, 249
252 (x,y2) e z2 <=> x e z & y2 e z
U Spec, 244
253 [(x,y2) e z2 => x e z & y2 e z]
& [x e z & y2 e z => (x,y2) e z2]
Iff-And, 252
254 (x,y2) e z2 => x e z & y2 e z
Split, 253
255 x e z & y2 e z => (x,y2) e z2
Split, 253
256 x e z & y2 e z
Detach, 254, 242
257 x e z
Split, 256
258 y2 e z
Split, 256
Two cases:
259 x e zright | ~x e zright
Or Not
Case 1
Suppose...
260 x e zright
Premise
261 ~[x e zright & y1 e zright & f(x)=y1] => ~x e zright & y1 e zleft & g(y1)=x
Imply-Or, 236
262 ~[~x e zright & y1 e zleft & g(y1)=x] => ~~[x e zright & y1 e zright & f(x)=y1]
Contra, 261
263 ~[~x e zright & y1 e zleft & g(y1)=x] => x e zright & y1 e zright & f(x)=y1
Rem DNeg, 262
Suppose to the contrary...
264 ~x e zright & y1 e zleft & g(y1)=x
Premise
265 ~x e zright
Split, 264
266 y1 e zleft
Split, 264
267 g(y1)=x
Split, 264
268 x e zright & ~x e zright
Join, 260, 265
269 ~[~x e zright & y1 e zleft & g(y1)=x]
4 Conclusion, 264
270 x e zright & y1 e zright & f(x)=y1
Detach, 263, 269
271 x e zright
Split, 270
272 y1 e zright
Split, 270
273 f(x)=y1
Split, 270
274 ~[x e zright & y2 e zright & f(x)=y2] => ~x e zright & y2 e zleft & g(y2)=x
Imply-Or, 243
275 ~[~x e zright & y2 e zleft & g(y2)=x] => ~~[x e zright & y2 e zright & f(x)=y2]
Contra, 274
276 ~[~x e zright & y2 e zleft & g(y2)=x] => x e zright & y2 e zright & f(x)=y2
Rem DNeg, 275
277 ~x e zright & y2 e zleft & g(y2)=x
Premise
278 ~x e zright
Split, 277
279 y2 e zleft
Split, 277
280 g(y2)=x
Split, 277
281 x e zright & ~x e zright
Join, 260, 278
282 ~[~x e zright & y2 e zleft & g(y2)=x]
4 Conclusion, 277
283 x e zright & y2 e zright & f(x)=y2
Detach, 276, 282
284 x e zright
Split, 283
285 y2 e zright
Split, 283
286 f(x)=y2
Split, 283
287 y1=y2
Substitute, 273, 286
As Required:
288 x e zright => y1=y2
4 Conclusion, 260
Case 2
Prove: ~x e zright => y1=y2
Suppose...
289 ~x e zright
Premise
290 ~[x e zright & y1 e zright & f(x)=y1] => ~x e zright & y1 e zleft & g(y1)=x
Imply-Or, 236
Prove: ~[x e zright & y1 e zright & f(x)=y1]
Suppose to the contrary...
291 x e zright & y1 e zright & f(x)=y1
Premise
292 x e zright
Split, 291
293 y1 e zright
Split, 291
294 f(x)=y1
Split, 291
295 x e zright & ~x e zright
Join, 292, 289
As Required:
296 ~[x e zright & y1 e zright & f(x)=y1]
4 Conclusion, 291
297 ~x e zright & y1 e zleft & g(y1)=x
Detach, 290, 296
298 ~x e zright
Split, 297
299 y1 e zleft
Split, 297
300 g(y1)=x
Split, 297
301 ~[x e zright & y2 e zright & f(x)=y2] => ~x e zright & y2 e zleft & g(y2)=x
Imply-Or, 243
Prove: ~[x e zright & y2 e zright & f(x)=y2]
Suppose to the contrary...
302 x e zright & y2 e zright & f(x)=y2
Premise
303 x e zright
Split, 302
304 y2 e zright
Split, 302
305 f(x)=y2
Split, 302
306 x e zright & ~x e zright
Join, 303, 289
As Required:
307 ~[x e zright & y2 e zright & f(x)=y2]
4 Conclusion, 302
308 ~x e zright & y2 e zleft & g(y2)=x
Detach, 301, 307
309 ~x e zright
Split, 308
310 y2 e zleft
Split, 308
311 g(y2)=x
Split, 308
312 g(y1)=g(y2)
Substitute, 311, 300
313 ALL(c):[y1 e zleft & c e zleft => [g(y1)=g(c) => y1=c]]
U Spec, 54
314 y1 e zleft & y2 e zleft => [g(y1)=g(y2) => y1=y2]
U Spec, 313
315 y1 e zleft & y2 e zleft
Join, 299, 310
316 g(y1)=g(y2) => y1=y2
Detach, 314, 315
317 y1=y2
Detach, 316, 312
As Required:
318 ~x e zright => y1=y2
4 Conclusion, 289
319 [x e zright => y1=y2] & [~x e zright => y1=y2]
Join, 288, 318
320 y1=y2
Cases, 259, 319
Functionality of next, Part 3
321 ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
4 Conclusion, 226
322 ALL(c):ALL(d):[(c,d) e next => c e z & d e z]
& ALL(c):[c e z => EXIST(d):[d e z & (c,d) e next]]
Join, 155, 225
323 ALL(c):ALL(d):[(c,d) e next => c e z & d e z]
& ALL(c):[c e z => EXIST(d):[d e z & (c,d) e next]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e next & (c,d2) e next => d1=d2]
Join, 322, 321
next is a function
324 ALL(c):ALL(d):[d=next(c) <=> (c,d) e next]
Detach, 140, 323
Prove: ALL(a):[a e z => next(a) e z]
Suppose...
325 x e z
Premise
326 x e z => EXIST(d):[d e z & (x,d) e next]
U Spec, 225
327 EXIST(d):[d e z & (x,d) e next]
Detach, 326, 325
328 y e z & (x,y) e next
E Spec, 327
329 y e z
Split, 328
330 (x,y) e next
Split, 328
331 ALL(d):[d=next(x) <=> (x,d) e next]
U Spec, 324
332 y=next(x) <=> (x,y) e next
U Spec, 331
333 [y=next(x) => (x,y) e next]
& [(x,y) e next => y=next(x)]
Iff-And, 332
334 y=next(x) => (x,y) e next
Split, 333
335 (x,y) e next => y=next(x)
Split, 333
336 y=next(x)
Detach, 335, 330
337 next(x) e z
Substitute, 336, 329
next is function on z
As Required:
338 ALL(a):[a e z => next(a) e z]
4 Conclusion, 325
Prove: ALL(a):[a e zright => a e z]
Suppose...
339 x e zright
Premise
340 x e z <=> x e zright | x e zleft
U Spec, 65
341 [x e z => x e zright | x e zleft]
& [x e zright | x e zleft => x e z]
Iff-And, 340
342 x e z => x e zright | x e zleft
Split, 341
343 x e zright | x e zleft => x e z
Split, 341
344 x e zright | x e zleft
Arb Or, 339
345 x e z
Detach, 343, 344
Lemma 7
346 ALL(a):[a e zright => a e z]
4 Conclusion, 339
Prove: ALL(a):[a e zleft => a e z]
Suppose...
347 x e zleft
Premise
348 x e z <=> x e zright | x e zleft
U Spec, 65
349 [x e z => x e zright | x e zleft]
& [x e zright | x e zleft => x e z]
Iff-And, 348
350 x e z => x e zright | x e zleft
Split, 349
351 x e zright | x e zleft => x e z
Split, 349
352 x e zright | x e zleft
Arb Or, 347
353 x e z
Detach, 351, 352
Lemma 8
354 ALL(a):[a e zleft => a e z]
4 Conclusion, 347
Prove: ALL(a):[a e zright => next(a)=f(a)]
Suppose...
355 x e zright
Premise
356 ALL(b):[(x,b) e next <=> (x,b) e z2 & [x e zright & b e zright & f(x)=b | ~x e zright & b e zleft & g(b)=x]]
U Spec, 136
357 (x,f(x)) e next <=> (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
U Spec, 356
358 [(x,f(x)) e next => (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]]
& [(x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x] => (x,f(x)) e next]
Iff-And, 357
359 (x,f(x)) e next => (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
Split, 358
Sufficient: For (x,f(x)) e next
360 (x,f(x)) e z2 & [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x] => (x,f(x)) e next
Split, 358
361 ALL(c2):[(x,c2) e z2 <=> x e z & c2 e z]
U Spec, 132
362 (x,f(x)) e z2 <=> x e z & f(x) e z
U Spec, 361
363 [(x,f(x)) e z2 => x e z & f(x) e z]
& [x e z & f(x) e z => (x,f(x)) e z2]
Iff-And, 362
364 (x,f(x)) e z2 => x e z & f(x) e z
Split, 363
365 x e z & f(x) e z => (x,f(x)) e z2
Split, 363
366 x e zright => x e z
U Spec, 346
367 x e z
Detach, 366, 355
368 x e zright => f(x) e zright
U Spec, 36
369 f(x) e zright
Detach, 368, 355
370 f(x) e zright => f(x) e z
U Spec, 346
371 f(x) e z
Detach, 370, 369
372 x e z & f(x) e z
Join, 367, 371
373 (x,f(x)) e z2
Detach, 365, 372
374 f(x)=f(x)
Reflex
375 x e zright & f(x) e zright
Join, 355, 369
376 x e zright & f(x) e zright & f(x)=f(x)
Join, 375, 374
377 x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x
Arb Or, 376
378 (x,f(x)) e z2
& [x e zright & f(x) e zright & f(x)=f(x) | ~x e zright & f(x) e zleft & g(f(x))=x]
Join, 373, 377
379 (x,f(x)) e next
Detach, 360, 378
380 ALL(d):[d=next(x) <=> (x,d) e next]
U Spec, 324
381 f(x)=next(x) <=> (x,f(x)) e next
U Spec, 380
382 [f(x)=next(x) => (x,f(x)) e next]
& [(x,f(x)) e next => f(x)=next(x)]
Iff-And, 381
383 f(x)=next(x) => (x,f(x)) e next
Split, 382
384 (x,f(x)) e next => f(x)=next(x)
Split, 382
385 f(x)=next(x)
Detach, 384, 379
386 next(x)=f(x)
Sym, 385
Lemma 9
387 ALL(a):[a e zright => next(a)=f(a)]
4 Conclusion, 355
Suppose...
388 x e z
Premise
389 x e zright | ~x e zright
Or Not
390 x e zright
Premise
391 x=0 | ~x=0
Or Not
392 x=0
Premise
393 ALL(b):[(g(0),b) e next <=> (g(0),b) e z2 & [g(0) e zright & b e zright & f(g(0))=b | ~g(0) e zright & b e zleft & g(b)=g(0)]]
U Spec, 136
394 (g(0),0) e next <=> (g(0),0) e z2 & [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)]
U Spec, 393
395 [(g(0),0) e next => (g(0),0) e z2 & [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)]]
& [(g(0),0) e z2 & [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)] => (g(0),0) e next]
Iff-And, 394
396 (g(0),0) e next => (g(0),0) e z2 & [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)]
Split, 395
Sufficient: For (g(0),0) e next
397 (g(0),0) e z2 & [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)] => (g(0),0) e next
Split, 395
398 ALL(c2):[(g(0),c2) e z2 <=> g(0) e z & c2 e z]
U Spec, 132
399 (g(0),0) e z2 <=> g(0) e z & 0 e z
U Spec, 398
400 [(g(0),0) e z2 => g(0) e z & 0 e z]
& [g(0) e z & 0 e z => (g(0),0) e z2]
Iff-And, 399
401 (g(0),0) e z2 => g(0) e z & 0 e z
Split, 400
402 g(0) e z & 0 e z => (g(0),0) e z2
Split, 400
403 0 e zleft => g(0) e zleft
U Spec, 53
404 g(0) e zleft
Detach, 403, 52
405 g(0) e zleft => g(0) e z
U Spec, 354
406 g(0) e z
Detach, 405, 404
407 g(0) e z & 0 e z
Join, 406, 71
408 (g(0),0) e z2
Detach, 402, 407
409 g(0) e zright
Premise
410 0 e zleft => g(0) e zleft
U Spec, 53
411 g(0) e zleft
Detach, 410, 52
412 g(0) e zright & g(0) e zleft <=> g(0)=0
U Spec, 92
413 [g(0) e zright & g(0) e zleft => g(0)=0]
& [g(0)=0 => g(0) e zright & g(0) e zleft]
Iff-And, 412
414 g(0) e zright & g(0) e zleft => g(0)=0
Split, 413
415 g(0)=0 => g(0) e zright & g(0) e zleft
Split, 413
416 g(0) e zright & g(0) e zleft
Join, 409, 411
417 g(0)=0
Detach, 414, 416
418 0 e zleft => ~g(0)=0
U Spec, 55
419 ~g(0)=0
Detach, 418, 52
420 g(0)=0 & ~g(0)=0
Join, 417, 419
421 ~g(0) e zright
4 Conclusion, 409
422 g(0)=g(0)
Reflex
423 ~g(0) e zright & 0 e zleft
Join, 421, 52
424 ~g(0) e zright & 0 e zleft & g(0)=g(0)
Join, 423, 422
425 g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)
Arb Or, 424
426 (g(0),0) e z2
& [g(0) e zright & 0 e zright & f(g(0))=0 | ~g(0) e zright & 0 e zleft & g(0)=g(0)]
Join, 408, 425
427 (g(0),0) e next
Detach, 397, 426
428 ALL(d):[d=next(g(0)) <=> (g(0),d) e next]
U Spec, 324
429 0=next(g(0)) <=> (g(0),0) e next
U Spec, 428
430 [0=next(g(0)) => (g(0),0) e next]
& [(g(0),0) e next => 0=next(g(0))]
Iff-And, 429
431 0=next(g(0)) => (g(0),0) e next
Split, 430
432 (g(0),0) e next => 0=next(g(0))
Split, 430
433 0=next(g(0))
Detach, 432, 427
434 next(g(0))=0
Sym, 433
435 g(0) e z & next(g(0))=0
Join, 406, 434
436 EXIST(b):[b e z & next(b)=0]
E Gen, 435
437 EXIST(b):[b e z & next(b)=x]
Substitute, 392, 436
438 x=0 => EXIST(b):[b e z & next(b)=x]
4 Conclusion, 392
439 ~x=0
Premise
440 ALL(s1):ALL(f):[Set(zright)
& s1 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=s1]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& s1 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
=> ALL(a):[a e zright => [~a=s1 => EXIST(b):[b e zright & f(b)=a]]]]
U Spec, 2
441 ALL(f):[Set(zright)
& 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
=> ALL(a):[a e zright => [~a=0 => EXIST(b):[b e zright & f(b)=a]]]]
U Spec, 440
442 Set(zright)
& 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
=> ALL(a):[a e zright => [~a=0 => EXIST(b):[b e zright & f(b)=a]]]
U Spec, 441
443 Set(zright) & 0 e zright
Join, 33, 35
444 Set(zright) & 0 e zright
& ALL(b):[b e zright => f(b) e zright]
Join, 443, 36
445 Set(zright) & 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
Join, 444, 37
446 Set(zright) & 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=0]
Join, 445, 38
447 Set(zright) & 0 e zright
& ALL(b):[b e zright => f(b) e zright]
& ALL(b):ALL(c):[b e zright & c e zright => [f(b)=f(c) => b=c]]
& ALL(b):[b e zright => ~f(b)=0]
& ALL(b):[Set(b)
& ALL(c):[c e b => c e zright]
& 0 e b
& ALL(c):[c e b => f(c) e b]
=> ALL(c):[c e zright => c e b]]
Join, 446, 39
448 ALL(a):[a e zright => [~a=0 => EXIST(b):[b e zright & f(b)=a]]]
Detach, 442, 447
449 x e zright => [~x=0 => EXIST(b):[b e zright & f(b)=x]]
U Spec, 448
450 ~x=0 => EXIST(b):[b e zright & f(b)=x]
Detach, 449, 390
451 EXIST(b):[b e zright & f(b)=x]
Detach, 450, 439
452 y e zright & f(y)=x
E Spec, 451
453 y e zright
Split, 452
454 f(y)=x
Split, 452
455 y e zright => next(y)=f(y)
U Spec, 387
456 next(y)=f(y)
Detach, 455, 453
457 next(y)=x
Substitute, 454, 456
458 y e zright => y e z
U Spec, 346
459 y e z
Detach, 458, 453
460 y e z & next(y)=x
Join, 459, 457
461 EXIST(b):[b e z & next(b)=x]
E Gen, 460
462 ~x=0 => EXIST(b):[b e z & next(b)=x]
4 Conclusion, 439
463 [x=0 => EXIST(b):[b e z & next(b)=x]]
& [~x=0 => EXIST(b):[b e z & next(b)=x]]
Join, 438, 462
464 EXIST(b):[b e z & next(b)=x]
Cases, 391, 463
465 x e zright => EXIST(b):[b e z & next(b)=x]
4