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 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