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 Conclusion, 390
466 ~x e zright
Premise
467 x e z => [~x e zright => x e zleft & ~x=0]
U Spec, 108
468 ~x e zright => x e zleft & ~x=0
Detach, 467, 388
469 x e zleft & ~x=0
Detach, 468, 466
470 x e zleft
Split, 469
471 ~x=0
Split, 469
472 ALL(b):[(g(x),b) e next <=> (g(x),b) e z2 & [g(x) e zright & b e zright & f(g(x))=b | ~g(x) e zright & b e zleft & g(b)=g(x)]]
U Spec, 136
473 (g(x),x) e next <=> (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
U Spec, 472
474 [(g(x),x) e next => (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]]
& [(g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)] => (g(x),x) e next]
Iff-And, 473
475 (g(x),x) e next => (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
Split, 474
Sufficient: (g(x),x) e next
476 (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)] => (g(x),x) e next
Split, 474
477 ALL(c2):[(g(x),c2) e z2 <=> g(x) e z & c2 e z]
U Spec, 132
478 (g(x),x) e z2 <=> g(x) e z & x e z
U Spec, 477
479 [(g(x),x) e z2 => g(x) e z & x e z]
& [g(x) e z & x e z => (g(x),x) e z2]
Iff-And, 478
480 (g(x),x) e z2 => g(x) e z & x e z
Split, 479
481 g(x) e z & x e z => (g(x),x) e z2
Split, 479
482 x e zleft => g(x) e zleft
U Spec, 53
483 g(x) e zleft
Detach, 482, 470
484 g(x) e zleft => g(x) e z
U Spec, 354
485 g(x) e z
Detach, 484, 483
486 g(x) e z & x e z
Join, 485, 388
487 (g(x),x) e z2
Detach, 481, 486
488 g(x) e zright & g(x) e zleft <=> g(x)=0
U Spec, 92
489 [g(x) e zright & g(x) e zleft => g(x)=0]
& [g(x)=0 => g(x) e zright & g(x) e zleft]
Iff-And, 488
490 g(x) e zright & g(x) e zleft => g(x)=0
Split, 489
491 g(x)=0 => g(x) e zright & g(x) e zleft
Split, 489
492 ~g(x)=0 => ~[g(x) e zright & g(x) e zleft]
Contra, 490
493 ~g(x)=0 => ~~[g(x) e zright => ~g(x) e zleft]
Imply-And, 492
494 ~g(x)=0 => [g(x) e zright => ~g(x) e zleft]
Rem DNeg, 493
495 ~g(x)=0 => [~~g(x) e zleft => ~g(x) e zright]
Contra, 494
496 ~g(x)=0 => [g(x) e zleft => ~g(x) e zright]
Rem DNeg, 495
497 x e zleft => ~g(x)=0
U Spec, 55
498 ~g(x)=0
Detach, 497, 470
499 g(x) e zleft => ~g(x) e zright
Detach, 496, 498
500 ~g(x) e zright
Detach, 499, 483
501 g(x)=g(x)
Reflex
502 ~g(x) e zright & x e zleft
Join, 500, 470
503 ~g(x) e zright & x e zleft & g(x)=g(x)
Join, 502, 501
504 g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)
Arb Or, 503
505 (g(x),x) e z2
& [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
Join, 487, 504
506 (g(x),x) e next
Detach, 476, 505
507 ALL(d):[d=next(g(x)) <=> (g(x),d) e next]
U Spec, 324
508 x=next(g(x)) <=> (g(x),x) e next
U Spec, 507
509 [x=next(g(x)) => (g(x),x) e next]
& [(g(x),x) e next => x=next(g(x))]
Iff-And, 508
510 x=next(g(x)) => (g(x),x) e next
Split, 509
511 (g(x),x) e next => x=next(g(x))
Split, 509
512 x=next(g(x))
Detach, 511, 506
513 next(g(x))=x
Sym, 512
514 g(x) e z & next(g(x))=x
Join, 485, 513
515 EXIST(b):[b e z & next(b)=x]
E Gen, 514
516 ~x e zright => EXIST(b):[b e z & next(b)=x]
4 Conclusion, 466
517 [x e zright => EXIST(b):[b e z & next(b)=x]]
& [~x e zright => EXIST(b):[b e z & next(b)=x]]
Join, 465, 516
518 EXIST(b):[b e z & next(b)=x]
Cases, 389, 517
next is surjective
519 ALL(a):[a e z => EXIST(b):[b e z & next(b)=a]]
4 Conclusion, 388
Prove: ALL(a1):ALL(a2):ALL(b):[a1 e z & a2 e z & b e z
=> [next(a1)=b & next(a2)=b => a1=a2]]
Suppose...
520 x1 e z & x2 e z & y e z
Premise
521 x1 e z
Split, 520
522 x2 e z
Split, 520
523 y e z
Split, 520
524 next(x1)=y & next(x2)=y
Premise
525 next(x1)=y
Split, 524
526 next(x2)=y
Split, 524
527 ALL(d):[d=next(x1) <=> (x1,d) e next]
U Spec, 324
528 y=next(x1) <=> (x1,y) e next
U Spec, 527
529 [y=next(x1) => (x1,y) e next]
& [(x1,y) e next => y=next(x1)]
Iff-And, 528
530 y=next(x1) => (x1,y) e next
Split, 529
531 (x1,y) e next => y=next(x1)
Split, 529
532 y=next(x1)
Sym, 525
533 (x1,y) e next
Detach, 530, 532
534 ALL(d):[d=next(x2) <=> (x2,d) e next]
U Spec, 324
535 y=next(x2) <=> (x2,y) e next
U Spec, 534
536 [y=next(x2) => (x2,y) e next]
& [(x2,y) e next => y=next(x2)]
Iff-And, 535
537 y=next(x2) => (x2,y) e next
Split, 536
538 (x2,y) e next => y=next(x2)
Split, 536
539 y=next(x2)
Sym, 526
540 (x2,y) e next
Detach, 537, 539
541 ALL(b):[(x1,b) e next <=> (x1,b) e z2 & [x1 e zright & b e zright & f(x1)=b | ~x1 e zright & b e zleft & g(b)=x1]]
U Spec, 136
542 (x1,y) e next <=> (x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1]
U Spec, 541
543 [(x1,y) e next => (x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1]]
& [(x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1] => (x1,y) e next]
Iff-And, 542
544 (x1,y) e next => (x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1]
Split, 543
545 (x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1] => (x1,y) e next
Split, 543
546 (x1,y) e z2 & [x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1]
Detach, 544, 533
547 (x1,y) e z2
Split, 546
548 x1 e zright & y e zright & f(x1)=y | ~x1 e zright & y e zleft & g(y)=x1
Split, 546
549 ALL(b):[(x2,b) e next <=> (x2,b) e z2 & [x2 e zright & b e zright & f(x2)=b | ~x2 e zright & b e zleft & g(b)=x2]]
U Spec, 136
550 (x2,y) e next <=> (x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2]
U Spec, 549
551 [(x2,y) e next => (x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2]]
& [(x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2] => (x2,y) e next]
Iff-And, 550
552 (x2,y) e next => (x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2]
Split, 551
553 (x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2] => (x2,y) e next
Split, 551
554 (x2,y) e z2 & [x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2]
Detach, 552, 540
555 (x2,y) e z2
Split, 554
556 x2 e zright & y e zright & f(x2)=y | ~x2 e zright & y e zleft & g(y)=x2
Split, 554
Two cases:
557 y e zright | ~y e zright
Or Not
558 y e zright
Premise
Two subcases:
559 y=0 | ~y=0
Or Not
560 y=0
Premise
561 x1 e zright & 0 e zright & f(x1)=0 | ~x1 e zright & 0 e zleft & g(0)=x1
Substitute, 560, 548
562 ~[x1 e zright & 0 e zright & f(x1)=0] => ~x1 e zright & 0 e zleft & g(0)=x1
Imply-Or, 561
Suppose to the contrary...
563 x1 e zright & 0 e zright & f(x1)=0
Premise
564 x1 e zright
Split, 563
565 0 e zright
Split, 563
566 f(x1)=0
Split, 563
567 x1 e zright => ~f(x1)=0
U Spec, 38
568 ~f(x1)=0
Detach, 567, 564
569 f(x1)=0 & ~f(x1)=0
Join, 566, 568
570 ~[x1 e zright & 0 e zright & f(x1)=0]
4 Conclusion, 563
571 ~x1 e zright & 0 e zleft & g(0)=x1
Detach, 562, 570
572 ~x1 e zright
Split, 571
573 0 e zleft
Split, 571
574 g(0)=x1
Split, 571
575 x2 e zright & 0 e zright & f(x2)=0 | ~x2 e zright & 0 e zleft & g(0)=x2
Substitute, 560, 556
576 ~[x2 e zright & 0 e zright & f(x2)=0] => ~x2 e zright & 0 e zleft & g(0)=x2
Imply-Or, 575
Suppose to the contrary...
577 x2 e zright & 0 e zright & f(x2)=0
Premise
578 x2 e zright
Split, 577
579 0 e zright
Split, 577
580 f(x2)=0
Split, 577
581 x2 e zright => ~f(x2)=0
U Spec, 38
582 ~f(x2)=0
Detach, 581, 578
583 f(x2)=0 & ~f(x2)=0
Join, 580, 582
584 ~[x2 e zright & 0 e zright & f(x2)=0]
4 Conclusion, 577
585 ~x2 e zright & 0 e zleft & g(0)=x2
Detach, 576, 584
586 ~x2 e zright
Split, 585
587 0 e zleft
Split, 585
588 g(0)=x2
Split, 585
589 x1=x2
Substitute, 574, 588
590 y=0 => x1=x2
4 Conclusion, 560
Case 2
Suppose...
591 ~y=0
Premise
592 ~[x1 e zright & y e zright & f(x1)=y] => ~x1 e zright & y e zleft & g(y)=x1
Imply-Or, 548
593 ~[~x1 e zright & y e zleft & g(y)=x1] => ~~[x1 e zright & y e zright & f(x1)=y]
Contra, 592
594 ~[~x1 e zright & y e zleft & g(y)=x1] => x1 e zright & y e zright & f(x1)=y
Rem DNeg, 593
Suppose to the contrary...
595 ~x1 e zright & y e zleft & g(y)=x1
Premise
596 ~x1 e zright
Split, 595
597 y e zleft
Split, 595
598 g(y)=x1
Split, 595
599 y e zright & y e zleft <=> y=0
U Spec, 92
600 [y e zright & y e zleft => y=0]
& [y=0 => y e zright & y e zleft]
Iff-And, 599
601 y e zright & y e zleft => y=0
Split, 600
602 y=0 => y e zright & y e zleft
Split, 600
603 y e zright & y e zleft
Join, 558, 597
604 y=0
Detach, 601, 603
605 y=0 & ~y=0
Join, 604, 591
606 ~[~x1 e zright & y e zleft & g(y)=x1]
4 Conclusion, 595
607 x1 e zright & y e zright & f(x1)=y
Detach, 594, 606
608 x1 e zright
Split, 607
609 y e zright
Split, 607
610 f(x1)=y
Split, 607
611 ~[x2 e zright & y e zright & f(x2)=y] => ~x2 e zright & y e zleft & g(y)=x2
Imply-Or, 556
612 ~[~x2 e zright & y e zleft & g(y)=x2] => ~~[x2 e zright & y e zright & f(x2)=y]
Contra, 611
613 ~[~x2 e zright & y e zleft & g(y)=x2] => x2 e zright & y e zright & f(x2)=y
Rem DNeg, 612
Suppose to the contrary...
614 ~x2 e zright & y e zleft & g(y)=x2
Premise
615 ~x2 e zright
Split, 614
616 y e zleft
Split, 614
617 g(y)=x2
Split, 614
618 y e zright & y e zleft <=> y=0
U Spec, 92
619 [y e zright & y e zleft => y=0]
& [y=0 => y e zright & y e zleft]
Iff-And, 618
620 y e zright & y e zleft => y=0
Split, 619
621 y=0 => y e zright & y e zleft
Split, 619
622 y e zright & y e zleft
Join, 609, 616
623 y=0
Detach, 620, 622
624 y=0 & ~y=0
Join, 623, 591
625 ~[~x2 e zright & y e zleft & g(y)=x2]
4 Conclusion, 614
626 x2 e zright & y e zright & f(x2)=y
Detach, 613, 625
627 x2 e zright
Split, 626
628 y e zright
Split, 626
629 f(x2)=y
Split, 626
630 f(x1)=f(x2)
Substitute, 629, 610
631 ALL(c):[x1 e zright & c e zright => [f(x1)=f(c) => x1=c]]
U Spec, 37
632 x1 e zright & x2 e zright => [f(x1)=f(x2) => x1=x2]
U Spec, 631
633 x1 e zright & x2 e zright
Join, 608, 627
634 f(x1)=f(x2) => x1=x2
Detach, 632, 633
635 x1=x2
Detach, 634, 630
636 ~y=0 => x1=x2
4 Conclusion, 591
637 [y=0 => x1=x2] & [~y=0 => x1=x2]
Join, 590, 636
638 x1=x2
Cases, 559, 637
639 y e zright => x1=x2
4 Conclusion, 558
640 ~y e zright
Premise
641 y e z => [~y e zright => y e zleft & ~y=0]
U Spec, 108
642 ~y e zright => y e zleft & ~y=0
Detach, 641, 523
643 y e zleft & ~y=0
Detach, 642, 640
644 y e zleft
Split, 643
645 ~y=0
Split, 643
646 ~[x1 e zright & y e zright & f(x1)=y] => ~x1 e zright & y e zleft & g(y)=x1
Imply-Or, 548
Suppose to the contrary...
647 x1 e zright & y e zright & f(x1)=y
Premise
648 x1 e zright
Split, 647
649 y e zright
Split, 647
650 f(x1)=y
Split, 647
651 y e zright & ~y e zright
Join, 649, 640
652 ~[x1 e zright & y e zright & f(x1)=y]
4 Conclusion, 647
653 ~x1 e zright & y e zleft & g(y)=x1
Detach, 646, 652
654 ~x1 e zright
Split, 653
655 y e zleft
Split, 653
656 g(y)=x1
Split, 653
657 ~[x2 e zright & y e zright & f(x2)=y] => ~x2 e zright & y e zleft & g(y)=x2
Imply-Or, 556
658 x2 e zright & y e zright & f(x2)=y
Premise
659 x2 e zright
Split, 658
660 y e zright
Split, 658
661 f(x2)=y
Split, 658
662 y e zright & ~y e zright
Join, 660, 640
663 ~[x2 e zright & y e zright & f(x2)=y]
4 Conclusion, 658
664 ~x2 e zright & y e zleft & g(y)=x2
Detach, 657, 663
665 ~x2 e zright
Split, 664
666 y e zleft
Split, 664
667 g(y)=x2
Split, 664
668 x1=x2
Substitute, 656, 667
669 ~y e zright => x1=x2
4 Conclusion, 640
670 [y e zright => x1=x2] & [~y e zright => x1=x2]
Join, 639, 669
671 x1=x2
Cases, 557, 670
672 next(x1)=y & next(x2)=y => x1=x2
4 Conclusion, 524
As Required:
673 ALL(a1):ALL(a2):ALL(b):[a1 e z & a2 e z & b e z
=> [next(a1)=b & next(a2)=b => a1=a2]]
4 Conclusion, 520
Prove: ALL(a):ALL(b):[a e z & b e z => [next(a)=next(b) => a=b]]
Suppose...
674 x1 e z & x2 e z
Premise
675 x1 e z
Split, 674
676 x2 e z
Split, 674
Prove: next(x1)=next(x2) => x1=x2
Suppose...
677 next(x1)=next(x2)
Premise
678 ALL(a2):ALL(b):[x1 e z & a2 e z & b e z
=> [next(x1)=b & next(a2)=b => x1=a2]]
U Spec, 673
679 ALL(b):[x1 e z & x2 e z & b e z
=> [next(x1)=b & next(x2)=b => x1=x2]]
U Spec, 678
680 x1 e z & x2 e z & next(x2) e z
=> [next(x1)=next(x2) & next(x2)=next(x2) => x1=x2]
U Spec, 679
681 x2 e z => next(x2) e z
U Spec, 338
682 next(x2) e z
Detach, 681, 676
683 x1 e z & x2 e z & next(x2) e z
Join, 674, 682
684 next(x1)=next(x2) & next(x2)=next(x2) => x1=x2
Detach, 680, 683
685 next(x2)=next(x2)
Reflex
686 next(x1)=next(x2) & next(x2)=next(x2)
Join, 677, 685
687 x1=x2
Detach, 684, 686
As Required:
688 next(x1)=next(x2) => x1=x2
4 Conclusion, 677
next is injective
As Required:
689 ALL(a):ALL(b):[a e z & b e z => [next(a)=next(b) => a=b]]
4 Conclusion, 674
690 ALL(y):ALL(f):[Set(z) & Set(y)
& ALL(a):[a e z => f(a) e y]
& ALL(a):[a e y => EXIST(b):[b e z & f(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e y => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e y => [f'(b)=a <=> f(a)=b]]]]
U Spec, 3
691 ALL(f):[Set(z) & Set(z)
& ALL(a):[a e z => f(a) e z]
& ALL(a):[a e z => EXIST(b):[b e z & f(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [f(a)=f(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e z => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [f'(b)=a <=> f(a)=b]]]]
U Spec, 690
692 Set(z) & Set(z)
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => EXIST(b):[b e z & next(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [next(a)=next(b) => a=b]]
=> EXIST(f'):[ALL(a):[a e z => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [f'(b)=a <=> next(a)=b]]]
U Spec, 691
693 Set(z) & Set(z)
Join, 64, 64
694 Set(z) & Set(z) & ALL(a):[a e z => next(a) e z]
Join, 693, 338
695 Set(z) & Set(z) & ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => EXIST(b):[b e z & next(b)=a]]
Join, 694, 519
696 Set(z) & Set(z) & ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => EXIST(b):[b e z & next(b)=a]]
& ALL(a):ALL(b):[a e z & b e z => [next(a)=next(b) => a=b]]
Join, 695, 689
697 EXIST(f'):[ALL(a):[a e z => f'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [f'(b)=a <=> next(a)=b]]]
Detach, 692, 696
698 ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
E Spec, 697
Define: next' (inverse of next)
*************
699 ALL(a):[a e z => next'(a) e z]
Split, 698
700 ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
Split, 698
Prove: ALL(a):[a e zleft => next'(a)=g(a)]
Suppose...
701 x e zleft
Premise
702 ALL(b):[(g(x),b) e next <=> (g(x),b) e z2 & [g(x) e zright & b e zright & f(g(x))=b | ~g(x) e zright & b e zleft & g(b)=g(x)]]
U Spec, 136
703 (g(x),x) e next <=> (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
U Spec, 702
704 [(g(x),x) e next => (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]]
& [(g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)] => (g(x),x) e next]
Iff-And, 703
705 (g(x),x) e next => (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
Split, 704
Sufficient: For (g(x),x) e next
706 (g(x),x) e z2 & [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)] => (g(x),x) e next
Split, 704
707 ALL(c2):[(g(x),c2) e z2 <=> g(x) e z & c2 e z]
U Spec, 132
708 (g(x),x) e z2 <=> g(x) e z & x e z
U Spec, 707
709 [(g(x),x) e z2 => g(x) e z & x e z]
& [g(x) e z & x e z => (g(x),x) e z2]
Iff-And, 708
710 (g(x),x) e z2 => g(x) e z & x e z
Split, 709
711 g(x) e z & x e z => (g(x),x) e z2
Split, 709
712 x e zleft => g(x) e zleft
U Spec, 53
713 g(x) e zleft
Detach, 712, 701
714 g(x) e zleft => g(x) e z
U Spec, 354
715 g(x) e z
Detach, 714, 713
716 x e zleft => x e z
U Spec, 354
717 x e z
Detach, 716, 701
718 g(x) e z & x e z
Join, 715, 717
719 (g(x),x) e z2
Detach, 711, 718
Prove: ~g(x) e zright
Suppose to the contrary...
720 g(x) e zright
Premise
721 g(x) e zright & g(x) e zleft <=> g(x)=0
U Spec, 92
722 [g(x) e zright & g(x) e zleft => g(x)=0]
& [g(x)=0 => g(x) e zright & g(x) e zleft]
Iff-And, 721
723 g(x) e zright & g(x) e zleft => g(x)=0
Split, 722
724 g(x)=0 => g(x) e zright & g(x) e zleft
Split, 722
725 g(x) e zright & g(x) e zleft
Join, 720, 713
726 g(x)=0
Detach, 723, 725
727 x e zleft => ~g(x)=0
U Spec, 55
728 ~g(x)=0
Detach, 727, 701
729 g(x)=0 & ~g(x)=0
Join, 726, 728
As Required:
730 ~g(x) e zright
4 Conclusion, 720
731 g(x)=g(x)
Reflex
732 ~g(x) e zright & x e zleft
Join, 730, 701
733 ~g(x) e zright & x e zleft & g(x)=g(x)
Join, 732, 731
734 g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)
Arb Or, 733
735 (g(x),x) e z2
& [g(x) e zright & x e zright & f(g(x))=x | ~g(x) e zright & x e zleft & g(x)=g(x)]
Join, 719, 734
736 (g(x),x) e next
Detach, 706, 735
737 ALL(d):[d=next(g(x)) <=> (g(x),d) e next]
U Spec, 324
738 x=next(g(x)) <=> (g(x),x) e next
U Spec, 737
739 [x=next(g(x)) => (g(x),x) e next]
& [(g(x),x) e next => x=next(g(x))]
Iff-And, 738
740 x=next(g(x)) => (g(x),x) e next
Split, 739
741 (g(x),x) e next => x=next(g(x))
Split, 739
742 x=next(g(x))
Detach, 741, 736
743 ALL(b):[g(x) e z & b e z => [next'(b)=g(x) <=> next(g(x))=b]]
U Spec, 700
744 g(x) e z & x e z => [next'(x)=g(x) <=> next(g(x))=x]
U Spec, 743
745 g(x) e z & x e z
Join, 715, 717
746 next'(x)=g(x) <=> next(g(x))=x
Detach, 744, 745
747 [next'(x)=g(x) => next(g(x))=x]
& [next(g(x))=x => next'(x)=g(x)]
Iff-And, 746
748 next'(x)=g(x) => next(g(x))=x
Split, 747
749 next(g(x))=x => next'(x)=g(x)
Split, 747
750 next(g(x))=x
Sym, 742
751 next'(x)=g(x)
Detach, 749, 750
As Required:
752 ALL(a):[a e zleft => next'(a)=g(a)]
4 Conclusion, 701
Prove: ALL(a):[a e zright => next(a) e zright]
Suppose...
753 x e zright
Premise
754 x e zright => next(x)=f(x)
U Spec, 387
755 next(x)=f(x)
Detach, 754, 753
756 x e zright => f(x) e zright
U Spec, 36
757 f(x) e zright
Detach, 756, 753
758 next(x) e zright
Substitute, 755, 757
next is closed on zright
As Required:
759 ALL(a):[a e zright => next(a) e zright]
4 Conclusion, 753
Prove: ALL(a):[a e zleft => next'(a) e zleft]
Suppose...
760 x e zleft
Premise
761 x e zleft => next'(x)=g(x)
U Spec, 752
762 next'(x)=g(x)
Detach, 761, 760
763 x e zleft => g(x) e zleft
U Spec, 53
764 g(x) e zleft
Detach, 763, 760
765 next'(x) e zleft
Substitute, 762, 764
next' is closed on zleft
As Required:
766 ALL(a):[a e zleft => next'(a) e zleft]
4 Conclusion, 760
Prove: ALL(a):[a e zright => ~next(a)=0]
Suppose...
767 x e zright
Premise
768 x e zright => ~f(x)=0
U Spec, 38
769 ~f(x)=0
Detach, 768, 767
770 x e zright => next(x)=f(x)
U Spec, 387
771 next(x)=f(x)
Detach, 770, 767
772 ~next(x)=0
Substitute, 771, 769
There is no pre-image of 0 in zright under next
As Required:
773 ALL(a):[a e zright => ~next(a)=0]
4 Conclusion, 767
Prove: ALL(x):[x e zleft => ~next'(x)=0]
Suppose...
774 x e zleft
Premise
775 x e zleft => ~g(x)=0
U Spec, 55
776 ~g(x)=0
Detach, 775, 774
777 x e zleft => next'(x)=g(x)
U Spec, 752
778 next'(x)=g(x)
Detach, 777, 774
779 ~next'(x)=0
Substitute, 778, 776
There is no pre-image of 0 in zleft under next'
As Required:
780 ALL(x):[x e zleft => ~next'(x)=0]
4 Conclusion, 774
Prove: ALL(a):[Set(a)
& ALL(b):[b e a => b e z]
& 0 e a
& ALL(b):[b e a => next(b) e a]
& ALL(b):[b e a => next'(b) e a]
=> ALL(c):[c e z => c e a]]
Suppose...
781 Set(p)
& ALL(b):[b e p => b e z]
& 0 e p
& ALL(b):[b e p => next(b) e p]
& ALL(b):[b e p => next'(b) e p]
Premise
782 Set(p)
Split, 781
783 ALL(b):[b e p => b e z]
Split, 781
784 0 e p
Split, 781
785 ALL(b):[b e p => next(b) e p]
Split, 781
786 ALL(b):[b e p => next'(b) e p]
Split, 781
Apply Subset Axiom
787 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e zright & a e p]]
Subset, 33
788 Set(pright) & ALL(a):[a e pright <=> a e zright & a e p]
E Spec, 787
Define: pright
789 Set(pright)
Split, 788
790 ALL(a):[a e pright <=> a e zright & a e p]
Split, 788
Apply induction on zright
791 Set(pright)
& ALL(c):[c e pright => c e zright]
& 0 e pright
& ALL(c):[c e pright => f(c) e pright]
=> ALL(c):[c e zright => c e pright]
U Spec, 39
Prove: ALL(c):[c e pright => c e zright]
Suppose...
792 x e pright
Premise
793 x e pright <=> x e zright & x e p
U Spec, 790
794 [x e pright => x e zright & x e p]
& [x e zright & x e p => x e pright]
Iff-And, 793
795 x e pright => x e zright & x e p
Split, 794
796 x e zright & x e p => x e pright
Split, 794
797 x e zright & x e p
Detach, 795, 792
798 x e zright
Split, 797
As Required:
799 ALL(c):[c e pright => c e zright]
4 Conclusion, 792
800 0 e pright <=> 0 e zright & 0 e p
U Spec, 790
801 [0 e pright => 0 e zright & 0 e p]
& [0 e zright & 0 e p => 0 e pright]
Iff-And, 800
802 0 e pright => 0 e zright & 0 e p
Split, 801
803 0 e zright & 0 e p => 0 e pright
Split, 801
804 0 e zright & 0 e p
Join, 35, 784
As Required:
805 0 e pright
Detach, 803, 804
Prove: ALL(c):[c e pright => f(c) e pright]
Suppose...
806 x e pright
Premise
807 x e pright <=> x e zright & x e p
U Spec, 790
808 [x e pright => x e zright & x e p]
& [x e zright & x e p => x e pright]
Iff-And, 807
809 x e pright => x e zright & x e p
Split, 808
810 x e zright & x e p => x e pright
Split, 808
811 x e zright & x e p
Detach, 809, 806
812 x e zright
Split, 811
813 x e p
Split, 811
814 x e p => next(x) e p
U Spec, 785
815 next(x) e p
Detach, 814, 813
816 x e zright => next(x)=f(x)
U Spec, 387
817 next(x)=f(x)
Detach, 816, 812
818 f(x) e pright <=> f(x) e zright & f(x) e p
U Spec, 790
819 [f(x) e pright => f(x) e zright & f(x) e p]
& [f(x) e zright & f(x) e p => f(x) e pright]
Iff-And, 818
820 f(x) e pright => f(x) e zright & f(x) e p
Split, 819
821 f(x) e zright & f(x) e p => f(x) e pright
Split, 819
822 x e zright => f(x) e zright
U Spec, 36
823 f(x) e zright
Detach, 822, 812
824 f(x) e p
Substitute, 817, 815
825 f(x) e zright & f(x) e p
Join, 823, 824
826 f(x) e pright
Detach, 821, 825
As Required:
827 ALL(c):[c e pright => f(c) e pright]
4 Conclusion, 806
828 Set(pright) & ALL(c):[c e pright => c e zright]
Join, 789, 799
829 Set(pright) & ALL(c):[c e pright => c e zright]
& 0 e pright
Join, 828, 805
830 Set(pright) & ALL(c):[c e pright => c e zright]
& 0 e pright
& ALL(c):[c e pright => f(c) e pright]
Join, 829, 827
831 ALL(c):[c e zright => c e pright]
Detach, 791, 830
832 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e zleft & a e p]]
Subset, 50
833 Set(pleft) & ALL(a):[a e pleft <=> a e zleft & a e p]
E Spec, 832
Define: pleft
834 Set(pleft)
Split, 833
835 ALL(a):[a e pleft <=> a e zleft & a e p]
Split, 833
Apply induction on pleft
836 Set(pleft)
& ALL(c):[c e pleft => c e zleft]
& 0 e pleft
& ALL(c):[c e pleft => g(c) e pleft]
=> ALL(c):[c e zleft => c e pleft]
U Spec, 56
Prove: ALL(c):[c e pleft => c e zleft]
Suppose...
837 x e pleft
Premise
838 x e pleft <=> x e zleft & x e p
U Spec, 835
839 [x e pleft => x e zleft & x e p]
& [x e zleft & x e p => x e pleft]
Iff-And, 838
840 x e pleft => x e zleft & x e p
Split, 839
841 x e zleft & x e p => x e pleft
Split, 839
842 x e zleft & x e p
Detach, 840, 837
843 x e zleft
Split, 842
As Required:
844 ALL(c):[c e pleft => c e zleft]
4 Conclusion, 837
845 0 e pleft <=> 0 e zleft & 0 e p
U Spec, 835
846 [0 e pleft => 0 e zleft & 0 e p]
& [0 e zleft & 0 e p => 0 e pleft]
Iff-And, 845
847 0 e pleft => 0 e zleft & 0 e p
Split, 846
Sufficient: 0 e pleft
848 0 e zleft & 0 e p => 0 e pleft
Split, 846
849 0 e zleft & 0 e p
Join, 52, 784
As Required:
850 0 e pleft
Detach, 848, 849
Prove: ALL(c):[c e pleft => g(c) e pleft]
Suppose...
851 x e pleft
Premise
852 x e pleft <=> x e zleft & x e p
U Spec, 835
853 [x e pleft => x e zleft & x e p]
& [x e zleft & x e p => x e pleft]
Iff-And, 852
854 x e pleft => x e zleft & x e p
Split, 853
855 x e zleft & x e p => x e pleft
Split, 853
856 x e zleft & x e p
Detach, 854, 851
857 x e zleft
Split, 856
858 x e p
Split, 856
859 g(x) e pleft <=> g(x) e zleft & g(x) e p
U Spec, 835
860 [g(x) e pleft => g(x) e zleft & g(x) e p]
& [g(x) e zleft & g(x) e p => g(x) e pleft]
Iff-And, 859
861 g(x) e pleft => g(x) e zleft & g(x) e p
Split, 860
Sufficient: For g(x) e pleft
862 g(x) e zleft & g(x) e p => g(x) e pleft
Split, 860
863 x e zleft => g(x) e zleft
U Spec, 53
864 g(x) e zleft
Detach, 863, 857
865 x e p => next'(x) e p
U Spec, 786
866 next'(x) e p
Detach, 865, 858
867 x e zleft => next'(x)=g(x)
U Spec, 752
868 next'(x)=g(x)
Detach, 867, 857
869 g(x) e p
Substitute, 868, 866
870 g(x) e zleft & g(x) e p
Join, 864, 869
871 g(x) e pleft
Detach, 862, 870
As Required:
872 ALL(c):[c e pleft => g(c) e pleft]
4 Conclusion, 851
873 Set(pleft) & ALL(c):[c e pleft => c e zleft]
Join, 834, 844
874 Set(pleft) & ALL(c):[c e pleft => c e zleft]
& 0 e pleft
Join, 873, 850
875 Set(pleft) & ALL(c):[c e pleft => c e zleft]
& 0 e pleft
& ALL(c):[c e pleft => g(c) e pleft]
Join, 874, 872
As Required:
876 ALL(c):[c e zleft => c e pleft]
Detach, 836, 875
Prove: ALL(c):[c e z => c e p]
Suppose...
877 x e z
Premise
878 x e z <=> x e zright | x e zleft
U Spec, 65
879 [x e z => x e zright | x e zleft]
& [x e zright | x e zleft => x e z]
Iff-And, 878
880 x e z => x e zright | x e zleft
Split, 879
881 x e zright | x e zleft => x e z
Split, 879
Two cases:
882 x e zright | x e zleft
Detach, 880, 877
Case 1
Prove: x e zright => x e p
Suppose...
883 x e zright
Premise
884 x e zright => x e pright
U Spec, 831
885 x e pright
Detach, 884, 883
886 x e pright <=> x e zright & x e p
U Spec, 790
887 [x e pright => x e zright & x e p]
& [x e zright & x e p => x e pright]
Iff-And, 886
888 x e pright => x e zright & x e p
Split, 887
889 x e zright & x e p => x e pright
Split, 887
890 x e zright & x e p
Detach, 888, 885
891 x e zright
Split, 890
892 x e p
Split, 890
As Required:
893 x e zright => x e p
4 Conclusion, 883
Prove: x e zleft => x e p
Suppose...
894 x e zleft
Premise
895 x e zleft => x e pleft
U Spec, 876
896 x e pleft
Detach, 895, 894
897 x e pleft <=> x e zleft & x e p
U Spec, 835
898 [x e pleft => x e zleft & x e p]
& [x e zleft & x e p => x e pleft]
Iff-And, 897
899 x e pleft => x e zleft & x e p
Split, 898
900 x e zleft & x e p => x e pleft
Split, 898
901 x e zleft & x e p
Detach, 899, 896
902 x e zleft
Split, 901
903 x e p
Split, 901
As Required:
904 x e zleft => x e p
4 Conclusion, 894
905 [x e zright => x e p] & [x e zleft => x e p]
Join, 893, 904
906 x e p
Cases, 882, 905
As Required:
907 ALL(c):[c e z => c e p]
4 Conclusion, 877
Induction on z
As Required:
908 ALL(a):[Set(a)
& ALL(b):[b e a => b e z]
& 0 e a
& ALL(b):[b e a => next(b) e a]
& ALL(b):[b e a => next'(b) e a]
=> ALL(c):[c e z => c e a]]
4 Conclusion, 781
Joining results...
909 Set(z) & Set(zright)
Join, 64, 33
910 Set(z) & Set(zright) & Set(zleft)
Join, 909, 50
911 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
Join, 910, 65
912 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
Join, 911, 92
913 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
Join, 912, 338
914 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
Join, 913, 699
915 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
Join, 914, 700
916 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
Join, 915, 759
917 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
& ALL(a):[a e zleft => next'(a) e zleft]
Join, 916, 766
918 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
& ALL(a):[a e zleft => next'(a) e zleft]
& ALL(a):[a e zright => ~next(a)=0]
Join, 917, 773
919 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
& ALL(a):[a e zleft => next'(a) e zleft]
& ALL(a):[a e zright => ~next(a)=0]
& ALL(x):[x e zleft => ~next'(x)=0]
Join, 918, 780
920 Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
& ALL(a):[a e zleft => next'(a) e zleft]
& ALL(a):[a e zright => ~next(a)=0]
& ALL(x):[x e zleft => ~next'(x)=0]
& ALL(a):[Set(a)
& ALL(b):[b e a => b e z]
& 0 e a
& ALL(b):[b e a => next(b) e a]
& ALL(b):[b e a => next'(b) e a]
=> ALL(c):[c e z => c e a]]
Join, 919, 908
As Required:
921 ALL(right):ALL(f):ALL(left):ALL(g):[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]]
=> EXIST(z):EXIST(zright):EXIST(zleft):EXIST(0):EXIST(next):EXIST(next'):[Set(z) & Set(zright) & Set(zleft)
& ALL(d):[d e z <=> d e zright | d e zleft]
& ALL(a):[a e zright & a e zleft <=> a=0]
& ALL(a):[a e z => next(a) e z]
& ALL(a):[a e z => next'(a) e z]
& ALL(a):ALL(b):[a e z & b e z => [next'(b)=a <=> next(a)=b]]
& ALL(a):[a e zright => next(a) e zright]
& ALL(a):[a e zleft => next'(a) e zleft]
& ALL(a):[a e zright => ~next(a)=0]
& ALL(x):[x e zleft => ~next'(x)=0]
& ALL(a):[Set(a)
& ALL(b):[b e a => b e z]
& 0 e a
& ALL(b):[b e a => next(b) e a]
& ALL(b):[b e a => next'(b) e a]
=> ALL(c):[c e z => c e a]]]]
4 Conclusion, 4