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

http://www.dcproof.com

 

 

 

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