THEOREM

*******

 

There are uncountable real numbers in the interval [0, 1)

 

OVERVIEW

********

 

We assume that every decimal of the form .d1 d2 d3 d4 ... (with the exception of .99999...) represents a real number in the interval [0, 1) on the real number line.

 

Each of these decimal expansions in turn can be represented by the obvious infinite string of digits -- simply drop the decimal point.

 

This is slightly complicated by situations like .0999999... = .1000000... since 0999999... and 1000000... are different strings of numbers. As such, we will consider the set t' of only those infinite strings of digits that do not end in an infinite string of all 9's. Here, we will prove only that the set of strings t' must uncountable.

 

For brevity, we will actually use base-3 in the following formal proof. The argument should be able to be extended for any base greater than 2, including base-10.)

 

CONTENTS

********

 

Previous result (with link): Line 1

 

Definitions: Lines 2 - 20

 

Establish sufficient condition for uncountability of t': Lines 21 - 123

 

Define an arbitrary function g: n --> t': Line 124

 

Establish sufficient condition for non-surjectivity of g: Lines 125 - 139

 

Construct anti-diagonal "string" h: Lines 140 - 142

 

Prove that h is the required "string" function: Lines 143 - 599

 

Prove that h e t': Lines 600 - 702

 

Prove that h is not in the range of g: Lines 703 - 793

 

Conclusion: 794 - 798

 

 

PREVIOUS RESULT 

***************

 

Countable if surjection from n  (see proof)

 

1     ALL(s):[Set(s) & EXIST(a):a e s

     => [Countable(s) => EXIST(f):[ALL(a):[a e n => f(a) e s] & Surjection(f,n,s)]]]

      Axiom

 

 

DEFINITIONS

***********

 

Define: Surjection

 

2     ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]

      Axiom

 

 

Let n be a set (the set of natural numbers)

 

3     Set(n)

      Axiom

 

 

Define: 0, 1, 2

 

4     0 e n

      Axiom

 

5     1 e n

      Axiom

 

6     1 e n

      Axiom

 

7     2 e n

      Axiom

 

8     ~0=1

      Axiom

 

9     ~0=2

      Axiom

 

10    ~1=2

      Axiom

 

 

Define: m  

*********

 

The set of digits for base-3 = {0, 1, 2}

 

11    Set(m)

      Axiom

 

12    ALL(a):[a e m <=> a=0 | a=1 | a=2]

      Axiom

 

 

Define: nm  (the Cartesian product of n and m)

**********

 

13    Set'(nm)

      Axiom

 

14    ALL(a):ALL(b):[(a,b) e nm <=> a e n & b e m]

      Axiom

 

 

Define: pnm  (the power set of nm)

***********

 

15    Set(pnm)

      Axiom

 

16    ALL(a):[a e pnm <=> Set'(a) & ALL(b):ALL(c):[(b,c) e a => (b,c) e nm]]

      Axiom

 

 

Define: f   (the "string" of all 0's)

*********

 

17    Set'(f)

      Axiom

 

18    ALL(a):ALL(b):[(a,b) e f <=> a e n & b=0]

      Axiom

 

 

Define: t' 

**********

 

The set of functions mapping n to m -- strings of 0's, 1's and 2's

that do not end in an infinite string of 2's (using base-3)

 

19    Set(t')

      Axiom

 

Each element of t' is a "string" of 0's, 1's and 2's, i.e. a mapping from N to {0, 1, 2} that does not end

in an infinite strings of 2's.  (For base-3)

 

20    ALL(a):[a e t' <=> a e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e a]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e a & (b,c2) e a => c1=c2]

     & ALL(b):[b e n => [(b,2) e a => EXIST(c):[c e n & [b<c & ~(c,2) e a]]]]]]

      Axiom

 

 

Establish sufficient condition for ~Countable(t')

 

Apply previous result

 

21    Set(t') & EXIST(a):a e t'

     => [Countable(t') => EXIST(f):[ALL(a):[a e n => f(a) e t'] & Surjection(f,n,t')]]

      U Spec, 1

 

22    Set(t') & EXIST(a):a e t'

     => [~EXIST(f):[ALL(a):[a e n => f(a) e t'] & Surjection(f,n,t')] => ~Countable(t')]

      Contra, 21

 

23    Set(t') & EXIST(a):a e t'

     => [~~ALL(f):~[ALL(a):[a e n => f(a) e t'] & Surjection(f,n,t')] => ~Countable(t')]

      Quant, 22

 

24    Set(t') & EXIST(a):a e t'

     => [ALL(f):~[ALL(a):[a e n => f(a) e t'] & Surjection(f,n,t')] => ~Countable(t')]

      Rem DNeg, 23

 

25    Set(t') & EXIST(a):a e t'

     => [ALL(f):~~[ALL(a):[a e n => f(a) e t'] => ~Surjection(f,n,t')] => ~Countable(t')]

      Imply-And, 24

 

26    Set(t') & EXIST(a):a e t'

     => [ALL(f):[ALL(a):[a e n => f(a) e t'] => ~Surjection(f,n,t')] => ~Countable(t')]

      Rem DNeg, 25

 

27    Set(t') & EXIST(a):a e t'

     => [Countable(t') => EXIST(f):[ALL(a):[a e n => f(a) e t'] & Surjection(f,n,t')]]

      U Spec, 1

 

Prove: f e t'

 

Apply definition of t'

 

28    f e t' <=> f e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]]

      U Spec, 20

 

29    [f e t' => f e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]]]

     & [f e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]] => f e t']

      Iff-And, 28

 

30    f e t' => f e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]]

      Split, 29

 

 

Sufficient:  For f e t'

 

31    f e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]] => f e t'

      Split, 29

 

Prove: f e pnm

 

Apply definition of pnm

 

32    f e pnm <=> Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]

      U Spec, 16

 

33    [f e pnm => Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]]

     & [Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm] => f e pnm]

      Iff-And, 32

 

34    f e pnm => Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]

      Split, 33

 

 

Sufficient: For f e pnm

 

35    Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm] => f e pnm

      Split, 33

 

    

     Prove: ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]

    

     Suppose...

 

      36    (x,y) e f

            Premise

 

     Apply definition of nm

 

      37    ALL(b):[(x,b) e nm <=> x e n & b e m]

            U Spec, 14

 

      38    (x,y) e nm <=> x e n & y e m

            U Spec, 37

 

      39    [(x,y) e nm => x e n & y e m]

          & [x e n & y e m => (x,y) e nm]

            Iff-And, 38

 

      40    (x,y) e nm => x e n & y e m

            Split, 39

 

     Sufficient: For (x,y) e nm

 

      41    x e n & y e m => (x,y) e nm

            Split, 39

 

     Apply definition of f

 

      42    ALL(b):[(x,b) e f <=> x e n & b=0]

            U Spec, 18

 

      43    (x,y) e f <=> x e n & y=0

            U Spec, 42

 

      44    [(x,y) e f => x e n & y=0] & [x e n & y=0 => (x,y) e f]

            Iff-And, 43

 

      45    (x,y) e f => x e n & y=0

            Split, 44

 

      46    x e n & y=0 => (x,y) e f

            Split, 44

 

      47    x e n & y=0

            Detach, 45, 36

 

      48    x e n

            Split, 47

 

      49    y=0

            Split, 47

 

     Apply definition of m

 

      50    y e m <=> y=0 | y=1 | y=2

            U Spec, 12

 

      51    [y e m => y=0 | y=1 | y=2] & [y=0 | y=1 | y=2 => y e m]

            Iff-And, 50

 

      52    y e m => y=0 | y=1 | y=2

            Split, 51

 

      53    y=0 | y=1 | y=2 => y e m

            Split, 51

 

      54    y=0 | y=1

            Arb Or, 49

 

      55    y=0 | y=1 | y=2

            Arb Or, 54

 

      56    y e m

            Detach, 53, 55

 

      57    x e n & y e m

            Join, 48, 56

 

      58    (x,y) e nm

            Detach, 41, 57

 

As Required:

 

59    ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]

      4 Conclusion, 36

 

60    Set'(f) & ALL(b):ALL(c):[(b,c) e f => (b,c) e nm]

      Join, 17, 59

 

As Required:

 

61    f e pnm

      Detach, 35, 60

 

    

     Prove: ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

    

     Suppose...

 

      62    x e n

            Premise

 

     Apply definition of f

 

      63    ALL(b):[(x,b) e f <=> x e n & b=0]

            U Spec, 18

 

      64    (x,0) e f <=> x e n & 0=0

            U Spec, 63

 

      65    [(x,0) e f => x e n & 0=0] & [x e n & 0=0 => (x,0) e f]

            Iff-And, 64

 

      66    (x,0) e f => x e n & 0=0

            Split, 65

 

      67    x e n & 0=0 => (x,0) e f

            Split, 65

 

      68    0=0

            Reflex

 

      69    x e n & 0=0

            Join, 62, 68

 

      70    (x,0) e f

            Detach, 67, 69

 

     Apply definition of m

 

      71    0 e m <=> 0=0 | 0=1 | 0=2

            U Spec, 12

 

      72    [0 e m => 0=0 | 0=1 | 0=2] & [0=0 | 0=1 | 0=2 => 0 e m]

            Iff-And, 71

 

      73    0 e m => 0=0 | 0=1 | 0=2

            Split, 72

 

      74    0=0 | 0=1 | 0=2 => 0 e m

            Split, 72

 

      75    0=0

            Reflex

 

      76    0=0 | 0=1

            Arb Or, 75

 

      77    0=0 | 0=1 | 0=2

            Arb Or, 76

 

      78    0 e m

            Detach, 74, 77

 

      79    0 e m & (x,0) e f

            Join, 78, 70

 

      80    EXIST(c):[c e m & (x,c) e f]

            E Gen, 79

 

As Required:

 

81    ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

      4 Conclusion, 62

 

    

     Prove: ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

    

     Suppose...

 

      82    (x,y1) e f & (x,y2) e f

            Premise

 

      83    (x,y1) e f

            Split, 82

 

      84    (x,y2) e f

            Split, 82

 

     Apply definition of f

 

      85    ALL(b):[(x,b) e f <=> x e n & b=0]

            U Spec, 18

 

      86    (x,y1) e f <=> x e n & y1=0

            U Spec, 85

 

      87    [(x,y1) e f => x e n & y1=0]

          & [x e n & y1=0 => (x,y1) e f]

            Iff-And, 86

 

      88    (x,y1) e f => x e n & y1=0

            Split, 87

 

      89    x e n & y1=0 => (x,y1) e f

            Split, 87

 

      90    x e n & y1=0

            Detach, 88, 83

 

      91    x e n

            Split, 90

 

      92    y1=0

            Split, 90

 

      93    (x,y2) e f <=> x e n & y2=0

            U Spec, 85

 

      94    [(x,y2) e f => x e n & y2=0]

          & [x e n & y2=0 => (x,y2) e f]

            Iff-And, 93

 

      95    (x,y2) e f => x e n & y2=0

            Split, 94

 

      96    x e n & y2=0 => (x,y2) e f

            Split, 94

 

      97    x e n & y2=0

            Detach, 95, 84

 

      98    x e n

            Split, 97

 

      99    y2=0

            Split, 97

 

      100  y1=y2

            Substitute, 99, 92

 

As Required:

 

101  ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

      4 Conclusion, 82

 

    

     Prove: ALL(b):[b e n

            => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]

    

     Suppose...

 

      102  x e n

            Premise

 

         

          Prove: (x,2) e f => EXIST(c):[c e n & [x<c & ~(c,2) e f]]

         

          Suppose...

 

            103  (x,2) e f

                  Premise

 

          Apply definition of f

 

            104  ALL(b):[(x,b) e f <=> x e n & b=0]

                  U Spec, 18

 

            105  (x,2) e f <=> x e n & 2=0

                  U Spec, 104

 

            106  [(x,2) e f => x e n & 2=0] & [x e n & 2=0 => (x,2) e f]

                  Iff-And, 105

 

            107  (x,2) e f => x e n & 2=0

                  Split, 106

 

            108  x e n & 2=0 => (x,2) e f

                  Split, 106

 

            109  x e n & 2=0

                  Detach, 107, 103

 

            110  x e n

                  Split, 109

 

            111  2=0

                  Split, 109

 

            112  0=2

                  Sym, 111

 

            113  ~0=2 => EXIST(c):[c e n & [x<c & ~(c,2) e f]]

                  Arb Cons, 112

 

            114  EXIST(c):[c e n & [x<c & ~(c,2) e f]]

                  Detach, 113, 9

 

     As Required:

 

      115  (x,2) e f => EXIST(c):[c e n & [x<c & ~(c,2) e f]]

            4 Conclusion, 103

 

As Required:

 

116  ALL(b):[b e n

     => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]

      4 Conclusion, 102

 

117  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

      Join, 81, 101

 

118  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n

     => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]

      Join, 117, 116

 

119  f e pnm

     & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e f]]

     & ALL(b):ALL(c1):ALL(c2):[(b,c1) e f & (b,c2) e f => c1=c2]

     & ALL(b):[b e n

     => [(b,2) e f => EXIST(c):[c e n & [b<c & ~(c,2) e f]]]]]

      Join, 61, 118

 

As Required:

 

120  f e t'

      Detach, 31, 119

 

 

As Required:

 

121  EXIST(a):a e t'

      E Gen, 120

 

 

Join results

 

122  Set(t') & EXIST(a):a e t'

      Join, 19, 121

 

 

Sufficient: For ~Countable(t')

 

123  ALL(f):[ALL(a):[a e n => f(a) e t'] => ~Surjection(f,n,t')] => ~Countable(t')

      Detach, 26, 122

 

    

     Prove: ALL(g):[ALL(a):[a e n => g(a) e t'] => ~Surjection(g,n,t')]

    

     Suppose...

 

      124  ALL(a):[a e n => g(a) e t']

            Premise

 

     Apply definition of Surjection

 

      125  ALL(a):ALL(b):[Surjection(g,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]

            U Spec, 2

 

      126  ALL(b):[Surjection(g,n,b) <=> ALL(c):[c e b => EXIST(d):[d e n & g(d)=c]]]

            U Spec, 125

 

      127  Surjection(g,n,t') <=> ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]]

            U Spec, 126

 

      128  [Surjection(g,n,t') => ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]]]

          & [ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]] => Surjection(g,n,t')]

            Iff-And, 127

 

      129  Surjection(g,n,t') => ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]]

            Split, 128

 

      130  ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]] => Surjection(g,n,t')

            Split, 128

 

      131  ~ALL(c):[c e t' => EXIST(d):[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Contra, 129

 

      132  ~~EXIST(c):~[c e t' => EXIST(d):[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Quant, 131

 

      133  EXIST(c):~[c e t' => EXIST(d):[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Rem DNeg, 132

 

      134  EXIST(c):~~[c e t' & ~EXIST(d):[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Imply-And, 133

 

      135  EXIST(c):[c e t' & ~EXIST(d):[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Rem DNeg, 134

 

      136  EXIST(c):[c e t' & ~~ALL(d):~[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Quant, 135

 

      137  EXIST(c):[c e t' & ALL(d):~[d e n & g(d)=c]] => ~Surjection(g,n,t')

            Rem DNeg, 136

 

      138  EXIST(c):[c e t' & ALL(d):~~[d e n => ~g(d)=c]] => ~Surjection(g,n,t')

            Imply-And, 137

 

    

     Sufficient: For ~Surjection(g,n,t')

    

     Use c=h (the anti-diagonal "string") as defined below

 

      139  EXIST(c):[c e t' & ALL(d):[d e n => ~g(d)=c]] => ~Surjection(g,n,t')

            Rem DNeg, 138

 

     Apply Subset Axiom

 

      140  EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e nm & [(a,0) e g(a) & b=1 | (a,1) e g(a) & b=0 | (a,2) e g(a) & b=0]]]

            Subset, 13

 

      141  Set'(h) & ALL(a):ALL(b):[(a,b) e h <=> (a,b) e nm & [(a,0) e g(a) & b=1 | (a,1) e g(a) & b=0 | (a,2) e g(a) & b=0]]

            E Spec, 140

 

    

     Define: h  (the anti-diagonal)

     *********

 

      142  Set'(h)

            Split, 141

 

      143  ALL(a):ALL(b):[(a,b) e h <=> (a,b) e nm & [(a,0) e g(a) & b=1 | (a,1) e g(a) & b=0 | (a,2) e g(a) & b=0]]

            Split, 141

 

     Apply Function Axiom

 

      144  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

 

      145  ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e h => c e a & d e b]

          & ALL(c):[c e a => EXIST(d):[d e b & (c,d) e h]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]

            U Spec, 144

 

      146  ALL(b):[ALL(c):ALL(d):[(c,d) e h => c e n & d e b]

          & ALL(c):[c e n => EXIST(d):[d e b & (c,d) e h]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]]

            U Spec, 145

 

    

     Sufficient: For functionality of h

 

      147  ALL(c):ALL(d):[(c,d) e h => c e n & d e m]

          & ALL(c):[c e n => EXIST(d):[d e m & (c,d) e h]]

          & ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]

          => ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]

            U Spec, 146

 

         

          Prove: ALL(c):ALL(d):[(c,d) e h => c e n & d e m]

         

          Suppose...

 

            148  (x,y) e h

                  Premise

 

          Apply definition of h

 

            149  ALL(b):[(x,b) e h <=> (x,b) e nm & [(x,0) e g(x) & b=1 | (x,1) e g(x) & b=0 | (x,2) e g(x) & b=0]]

                  U Spec, 143

 

            150  (x,y) e h <=> (x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0]

                  U Spec, 149

 

            151  [(x,y) e h => (x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0]]

              & [(x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0] => (x,y) e h]

                  Iff-And, 150

 

            152  (x,y) e h => (x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0]

                  Split, 151

 

            153  (x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0] => (x,y) e h

                  Split, 151

 

            154  (x,y) e nm & [(x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0]

                  Detach, 152, 148

 

            155  (x,y) e nm

                  Split, 154

 

            156  (x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0

                  Split, 154

 

          Apply definition of nm

 

            157  ALL(b):[(x,b) e nm <=> x e n & b e m]

                  U Spec, 14

 

            158  (x,y) e nm <=> x e n & y e m

                  U Spec, 157

 

            159  [(x,y) e nm => x e n & y e m]

              & [x e n & y e m => (x,y) e nm]

                  Iff-And, 158

 

            160  (x,y) e nm => x e n & y e m

                  Split, 159

 

            161  x e n & y e m => (x,y) e nm

                  Split, 159

 

            162  x e n & y e m

                  Detach, 160, 155

 

     As Required:

 

      163  ALL(c):ALL(d):[(c,d) e h => c e n & d e m]

            4 Conclusion, 148

 

         

          Prove: ALL(c):[c e n => EXIST(d):[d e m & (c,d) e h]]

         

          Suppose...

 

            164  x e n

                  Premise

 

          Apply definition of g

 

            165  x e n => g(x) e t'

                  U Spec, 124

 

          Let g(x) be the designated xth string in t'

 

            166  g(x) e t'

                  Detach, 165, 164

 

            167  g(x) e t' <=> g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                  U Spec, 20

 

            168  [g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]]

              & [g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t']

                  Iff-And, 167

 

            169  g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                  Split, 168

 

            170  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t'

                  Split, 168

 

            171  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                  Detach, 169, 166

 

            172  g(x) e pnm

                  Split, 171

 

            173  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

              & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

              & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                  Split, 171

 

            174  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                  Split, 173

 

            175  ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                  Split, 173

 

            176  ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                  Split, 173

 

          Apply definition of pnm

 

            177  g(x) e pnm <=> Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]

                  U Spec, 16

 

            178  [g(x) e pnm => Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]]

              & [Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm] => g(x) e pnm]

                  Iff-And, 177

 

            179  g(x) e pnm => Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]

                  Split, 178

 

            180  Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm] => g(x) e pnm

                  Split, 178

 

            181  Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]

                  Detach, 179, 172

 

            182  Set'(g(x))

                  Split, 181

 

          g(x) is a subset of nm

 

            183  ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]

                  Split, 181

 

          Apply previous result

 

            184  x e n => EXIST(c):[c e m & (x,c) e g(x)]

                  U Spec, 174

 

            185  EXIST(c):[c e m & (x,c) e g(x)]

                  Detach, 184, 164

 

            186  y e m & (x,y) e g(x)

                  E Spec, 185

 

         

          Define: y  (the image of x under g(x))

          *********

 

            187  y e m

                  Split, 186

 

            188  (x,y) e g(x)

                  Split, 186

 

            189  y e m <=> y=0 | y=1 | y=2

                  U Spec, 12

 

            190  [y e m => y=0 | y=1 | y=2] & [y=0 | y=1 | y=2 => y e m]

                  Iff-And, 189

 

            191  y e m => y=0 | y=1 | y=2

                  Split, 190

 

            192  y=0 | y=1 | y=2 => y e m

                  Split, 190

 

         

          Three cases to consider:

 

            193  y=0 | y=1 | y=2

                  Detach, 191, 187

 

             

              Case 1

             

              Prove: y=0 => EXIST(d):[d e m & (x,d) e h]

             

              Suppose...

 

                  194  y=0

                        Premise

 

              Apply definition of h

 

                  195  ALL(b):[(x,b) e h <=> (x,b) e nm & [(x,0) e g(x) & b=1 | (x,1) e g(x) & b=0 | (x,2) e g(x) & b=0]]

                        U Spec, 143

 

                  196  (x,1) e h <=> (x,1) e nm & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0]

                        U Spec, 195

 

                  197  [(x,1) e h => (x,1) e nm & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0]]

                   & [(x,1) e nm & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0] => (x,1) e h]

                        Iff-And, 196

 

                  198  (x,1) e h => (x,1) e nm & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0]

                        Split, 197

 

              Sufficient: For (x,1) e h

 

                  199  (x,1) e nm & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0] => (x,1) e h

                        Split, 197

 

              Prove: (x,1) e nm

             

              Apply definition of nm

 

                  200  ALL(b):[(x,b) e nm <=> x e n & b e m]

                        U Spec, 14

 

                  201  (x,1) e nm <=> x e n & 1 e m

                        U Spec, 200

 

                  202  [(x,1) e nm => x e n & 1 e m]

                   & [x e n & 1 e m => (x,1) e nm]

                        Iff-And, 201

 

                  203  (x,1) e nm => x e n & 1 e m

                        Split, 202

 

                  204  x e n & 1 e m => (x,1) e nm

                        Split, 202

 

              Apply definition of m

 

                  205  1 e m <=> 1=0 | 1=1 | 1=2

                        U Spec, 12

 

                  206  [1 e m => 1=0 | 1=1 | 1=2] & [1=0 | 1=1 | 1=2 => 1 e m]

                        Iff-And, 205

 

                  207  1 e m => 1=0 | 1=1 | 1=2

                        Split, 206

 

                  208  1=0 | 1=1 | 1=2 => 1 e m

                        Split, 206

 

                  209  1=1

                        Reflex

 

                  210  1=0 | 1=1

                        Arb Or, 209

 

                  211  1=0 | 1=1 | 1=2

                        Arb Or, 210

 

                  212  1 e m

                        Detach, 208, 211

 

                  213  x e n & 1 e m

                        Join, 164, 212

 

              As Required:

 

                  214  (x,1) e nm

                        Detach, 204, 213

 

                  215  (x,0) e g(x)

                        Substitute, 194, 188

 

                  216  1=1

                        Reflex

 

                  217  (x,0) e g(x) & 1=1

                        Join, 215, 216

 

                  218  (x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0

                        Arb Or, 217

 

                  219  (x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0

                        Arb Or, 218

 

                  220  (x,1) e nm

                   & [(x,0) e g(x) & 1=1 | (x,1) e g(x) & 1=0 | (x,2) e g(x) & 1=0]

                        Join, 214, 219

 

                  221  (x,1) e h

                        Detach, 199, 220

 

                  222  1 e m & (x,1) e h

                        Join, 212, 221

 

                  223  EXIST(d):[d e m & (x,d) e h]

                        E Gen, 222

 

          As Required:

 

            224  y=0 => EXIST(d):[d e m & (x,d) e h]

                  4 Conclusion, 194

 

             

              Case 2

             

              Prove: y=1 => EXIST(d):[d e m & (x,d) e h]

             

              Suppose...

 

                  225  y=1

                        Premise

 

              Apply definition of h

 

                  226  ALL(b):[(x,b) e h <=> (x,b) e nm & [(x,0) e g(x) & b=1 | (x,1) e g(x) & b=0 | (x,2) e g(x) & b=0]]

                        U Spec, 143

 

                  227  (x,0) e h <=> (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        U Spec, 226

 

                  228  [(x,0) e h => (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]]

                   & [(x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0] => (x,0) e h]

                        Iff-And, 227

 

                  229  (x,0) e h => (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        Split, 228

 

              Sufficient: For (x,0) e h

 

                  230  (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0] => (x,0) e h

                        Split, 228

 

              Prove: (x,0) e nm

             

              Apply definition of nm

 

                  231  ALL(b):[(x,b) e nm <=> x e n & b e m]

                        U Spec, 14

 

                  232  (x,0) e nm <=> x e n & 0 e m

                        U Spec, 231

 

                  233  [(x,0) e nm => x e n & 0 e m]

                   & [x e n & 0 e m => (x,0) e nm]

                        Iff-And, 232

 

                  234  (x,0) e nm => x e n & 0 e m

                        Split, 233

 

              Sufficient: For (x,0) e nm

 

                  235  x e n & 0 e m => (x,0) e nm

                        Split, 233

 

              Prove: 0 e m

             

              Apply definition of m

 

                  236  0 e m <=> 0=0 | 0=1 | 0=2

                        U Spec, 12

 

                  237  [0 e m => 0=0 | 0=1 | 0=2] & [0=0 | 0=1 | 0=2 => 0 e m]

                        Iff-And, 236

 

                  238  0 e m => 0=0 | 0=1 | 0=2

                        Split, 237

 

              Sufficient: For 0 e m

 

                  239  0=0 | 0=1 | 0=2 => 0 e m

                        Split, 237

 

                  240  0=0

                        Reflex

 

                  241  0=0 | 0=1

                        Arb Or, 240

 

                  242  0=0 | 0=1 | 0=2

                        Arb Or, 241

 

              As Required:

 

                  243  0 e m

                        Detach, 239, 242

 

                  244  x e n & 0 e m

                        Join, 164, 243

 

              As Required:

 

                  245  (x,0) e nm

                        Detach, 235, 244

 

                  246  (x,1) e g(x)

                        Substitute, 225, 188

 

                  247  0=0

                        Reflex

 

                  248  (x,1) e g(x) & 0=0

                        Join, 246, 247

 

                  249  (x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0

                        Arb Or, 248

 

                  250  (x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0

                        Arb Or, 249

 

                  251  (x,0) e nm

                   & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        Join, 245, 250

 

                  252  (x,0) e h

                        Detach, 230, 251

 

                  253  0 e m & (x,0) e h

                        Join, 243, 252

 

                  254  EXIST(d):[d e m & (x,d) e h]

                        E Gen, 253

 

          As Required:

 

            255  y=1 => EXIST(d):[d e m & (x,d) e h]

                  4 Conclusion, 225

 

             

              Case 3

             

              Prove: y=2 => EXIST(d):[d e m & (x,d) e h]

             

              Suppose...

 

                  256  y=2

                        Premise

 

                  257  ALL(b):[(x,b) e h <=> (x,b) e nm & [(x,0) e g(x) & b=1 | (x,1) e g(x) & b=0 | (x,2) e g(x) & b=0]]

                        U Spec, 143

 

                  258  (x,0) e h <=> (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        U Spec, 257

 

                  259  [(x,0) e h => (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]]

                   & [(x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0] => (x,0) e h]

                        Iff-And, 258

 

                  260  (x,0) e h => (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        Split, 259

 

              Sufficient: For (x,0) e h

 

                  261  (x,0) e nm & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0] => (x,0) e h

                        Split, 259

 

              Prove: (x,0) e nm

             

              Apply the definition of nm

 

                  262  ALL(b):[(x,b) e nm <=> x e n & b e m]

                        U Spec, 14

 

                  263  (x,0) e nm <=> x e n & 0 e m

                        U Spec, 262

 

                  264  (x,0) e nm <=> x e n & 0 e m

                        U Spec, 262

 

                  265  [(x,0) e nm => x e n & 0 e m]

                   & [x e n & 0 e m => (x,0) e nm]

                        Iff-And, 264

 

                  266  (x,0) e nm => x e n & 0 e m

                        Split, 265

 

              Sufficient: For (x,0) e nm

 

                  267  x e n & 0 e m => (x,0) e nm

                        Split, 265

 

              Prove: 0 e m

             

              Apply definition of m

 

                  268  0 e m <=> 0=0 | 0=1 | 0=2

                        U Spec, 12

 

                  269  [0 e m => 0=0 | 0=1 | 0=2] & [0=0 | 0=1 | 0=2 => 0 e m]

                        Iff-And, 268

 

                  270  0 e m => 0=0 | 0=1 | 0=2

                        Split, 269

 

                  271  0=0 | 0=1 | 0=2 => 0 e m

                        Split, 269

 

                  272  0=0

                        Reflex

 

                  273  0=0 | 0=1

                        Arb Or, 272

 

                  274  0=0 | 0=1 | 0=2

                        Arb Or, 273

 

              As Required:

 

                  275  0 e m

                        Detach, 271, 274

 

                  276  x e n & 0 e m

                        Join, 164, 275

 

              As Required:

 

                  277  (x,0) e nm

                        Detach, 267, 276

 

                  278  (x,2) e g(x)

                        Substitute, 256, 188

 

                  279  0=0

                        Reflex

 

                  280  (x,2) e g(x) & 0=0

                        Join, 278, 279

 

                  281  (x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0

                        Arb Or, 280

 

                  282  (x,0) e nm

                   & [(x,0) e g(x) & 0=1 | (x,1) e g(x) & 0=0 | (x,2) e g(x) & 0=0]

                        Join, 277, 281

 

                  283  (x,0) e h

                        Detach, 261, 282

 

                  284  0 e m & (x,0) e h

                        Join, 275, 283

 

                  285  EXIST(d):[d e m & (x,d) e h]

                        E Gen, 284

 

          As Required:

 

            286  y=2 => EXIST(d):[d e m & (x,d) e h]

                  4 Conclusion, 256

 

            287  [y=0 => EXIST(d):[d e m & (x,d) e h]]

              & [y=1 => EXIST(d):[d e m & (x,d) e h]]

                  Join, 224, 255

 

            288  [y=0 => EXIST(d):[d e m & (x,d) e h]]

              & [y=1 => EXIST(d):[d e m & (x,d) e h]]

              & [y=2 => EXIST(d):[d e m & (x,d) e h]]

                  Join, 287, 286

 

            289  EXIST(d):[d e m & (x,d) e h]

                  Cases, 193, 288

 

     As Required:

 

      290  ALL(c):[c e n => EXIST(d):[d e m & (c,d) e h]]

            4 Conclusion, 164

 

         

          Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]

         

          Suppose...

 

            291  (x,y1) e h & (x,y2) e h

                  Premise

 

            292  (x,y1) e h

                  Split, 291

 

            293  (x,y2) e h

                  Split, 291

 

          Apply definition of h

 

            294  ALL(b):[(x,b) e h <=> (x,b) e nm & [(x,0) e g(x) & b=1 | (x,1) e g(x) & b=0 | (x,2) e g(x) & b=0]]

                  U Spec, 143

 

            295  (x,y1) e h <=> (x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0]

                  U Spec, 294

 

            296  [(x,y1) e h => (x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0]]

              & [(x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0] => (x,y1) e h]

                  Iff-And, 295

 

            297  (x,y1) e h => (x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0]

                  Split, 296

 

            298  (x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0] => (x,y1) e h

                  Split, 296

 

            299  (x,y1) e nm & [(x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0]

                  Detach, 297, 292

 

            300  (x,y1) e nm

                  Split, 299

 

          Apply definition of nm

 

            301  ALL(b):[(x,b) e nm <=> x e n & b e m]

                  U Spec, 14

 

            302  (x,y1) e nm <=> x e n & y1 e m

                  U Spec, 301

 

            303  [(x,y1) e nm => x e n & y1 e m]

              & [x e n & y1 e m => (x,y1) e nm]

                  Iff-And, 302

 

            304  (x,y1) e nm => x e n & y1 e m

                  Split, 303

 

            305  x e n & y1 e m => (x,y1) e nm

                  Split, 303

 

            306  x e n & y1 e m

                  Detach, 304, 300

 

            307  x e n

                  Split, 306

 

            308  y1 e m

                  Split, 306

 

         

          Three cases to consider:

 

            309  (x,0) e g(x) & y1=1 | (x,1) e g(x) & y1=0 | (x,2) e g(x) & y1=0

                  Split, 299

 

            310  (x,y2) e h <=> (x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0]

                  U Spec, 294

 

            311  [(x,y2) e h => (x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0]]

              & [(x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0] => (x,y2) e h]

                  Iff-And, 310

 

            312  (x,y2) e h => (x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0]

                  Split, 311

 

            313  (x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0] => (x,y2) e h

                  Split, 311

 

            314  (x,y2) e nm & [(x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0]

                  Detach, 312, 293

 

            315  (x,y2) e nm

                  Split, 314

 

          Three sub-cases to consider:

 

            316  (x,0) e g(x) & y2=1 | (x,1) e g(x) & y2=0 | (x,2) e g(x) & y2=0

                  Split, 314

 

             

              Case 1

             

              Prove: (x,0) e g(x) & y1=1 => y1=y2

             

              Suppose...

 

                  317  (x,0) e g(x) & y1=1

                        Premise

 

                  318  (x,0) e g(x)

                        Split, 317

 

                  319  y1=1

                        Split, 317

 

                  

                   Sub-case 1

                  

                   Prove: (x,0) e g(x) & y2=1 => y1=y2

                  

                   Suppose...

 

                        320  (x,0) e g(x) & y2=1

                              Premise

 

                        321  (x,0) e g(x)

                              Split, 320

 

                        322  y2=1

                              Split, 320

 

                        323  y1=y2

                              Substitute, 322, 319

 

              As Required:

 

                  324  (x,0) e g(x) & y2=1 => y1=y2

                        4 Conclusion, 320

 

                  

                   Sub-case 2

                  

                   Prove: (x,1) e g(x) & y2=0 => y1=y2

                  

                   Suppose...

 

                        325  (x,1) e g(x) & y2=0

                              Premise

 

                        326  (x,1) e g(x)

                              Split, 325

 

                        327  y2=0

                              Split, 325

 

                   Apply definition of t'

 

                        328  g(x) e t' <=> g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              U Spec, 20

 

                        329  [g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]]

                        & [g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t']

                              Iff-And, 328

 

                        330  g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Split, 329

 

                        331  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t'

                              Split, 329

 

                   Apply definition of g

 

                        332  x e n => g(x) e t'

                              U Spec, 124

 

                        333  g(x) e t'

                              Detach, 332, 307

 

                        334  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Detach, 330, 333

 

                        335  g(x) e pnm

                              Split, 334

 

                        336  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 334

 

                        337  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                              Split, 336

 

                        338  ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                              Split, 336

 

                        339  ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 336

 

                        340  1 e n => [(1,2) e g(x) => EXIST(c):[c e n & [1<c & ~(c,2) e g(x)]]]

                              U Spec, 339

 

                        341  ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]

                              U Spec, 338

 

                        342  ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]

                              U Spec, 341

 

                        343  (x,0) e g(x) & (x,1) e g(x) => 0=1

                              U Spec, 342

 

                        344  (x,0) e g(x) & (x,1) e g(x)

                              Join, 318, 326

 

                        345  0=1

                              Detach, 343, 344

 

                        346  ~0=1 => y1=y2

                              Arb Cons, 345

 

                        347  y1=y2

                              Detach, 346, 8

 

              As Required:

 

                  348  (x,1) e g(x) & y2=0 => y1=y2

                        4 Conclusion, 325

 

                  

                   Sub-case 3

                  

                   Prove: (x,2) e g(x) & y2=0 => y1=y2

                  

                   Suppose...

 

                        349  (x,2) e g(x) & y2=0

                              Premise

 

                        350  (x,2) e g(x)

                              Split, 349

 

                        351  y2=0

                              Split, 349

 

                   Apply definition of t'

 

                        352  g(x) e t' <=> g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              U Spec, 20

 

                        353  [g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]]

                        & [g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t']

                              Iff-And, 352

 

                        354  g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Split, 353

 

                        355  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t'

                              Split, 353

 

                        356  [g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]]

                        & [g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t']

                              Iff-And, 352

 

                        357  g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Split, 356

 

                        358  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t'

                              Split, 356

 

                   Apply definition of g

 

                        359  x e n => g(x) e t'

                              U Spec, 124

 

                        360  g(x) e t'

                              Detach, 359, 307

 

                        361  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Detach, 357, 360

 

                        362  g(x) e pnm

                              Split, 361

 

                        363  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 361

 

                        364  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                              Split, 363

 

                        365  ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                              Split, 363

 

                        366  ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 363

 

                        367  ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]

                              U Spec, 365

 

                        368  ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]

                              U Spec, 367

 

                        369  (x,0) e g(x) & (x,2) e g(x) => 0=2

                              U Spec, 368

 

                        370  (x,0) e g(x) & (x,2) e g(x)

                              Join, 318, 350

 

                        371  0=2

                              Detach, 369, 370

 

                        372  ~0=2 => y1=y2

                              Arb Cons, 371

 

                        373  y1=y2

                              Detach, 372, 9

 

              As Required:

 

                  374  (x,2) e g(x) & y2=0 => y1=y2

                        4 Conclusion, 349

 

                  375  [(x,0) e g(x) & y2=1 => y1=y2]

                   & [(x,1) e g(x) & y2=0 => y1=y2]

                        Join, 324, 348

 

                  376  [(x,0) e g(x) & y2=1 => y1=y2]

                   & [(x,1) e g(x) & y2=0 => y1=y2]

                   & [(x,2) e g(x) & y2=0 => y1=y2]

                        Join, 375, 374

 

                  377  y1=y2

                        Cases, 316, 376

 

          As Required:

 

            378  (x,0) e g(x) & y1=1 => y1=y2

                  4 Conclusion, 317

 

             

              Case 2

             

              Prove: (x,1) e g(x) & y1=0 => y1=y2

             

              Suppose...

 

                  379  (x,1) e g(x) & y1=0

                        Premise

 

                  380  (x,1) e g(x)

                        Split, 379

 

                  381  y1=0

                        Split, 379

 

                  

                   Sub-case 1

                  

                   Prove: (x,0) e g(x) & y2=1 => y1=y2

                  

                   Suppose...

 

                        382  (x,0) e g(x) & y2=1

                              Premise

 

                        383  (x,0) e g(x)

                              Split, 382

 

                        384  y2=1

                              Split, 382

 

                   Apply definition of t'

 

                        385  g(x) e t' <=> g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              U Spec, 20

 

                        386  [g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]]

                        & [g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t']

                              Iff-And, 385

 

                        387  g(x) e t' => g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Split, 386

 

                        388  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]] => g(x) e t'

                              Split, 386

 

                   Apply definition of t'

 

                        389  x e n => g(x) e t'

                              U Spec, 124

 

                        390  g(x) e t'

                              Detach, 389, 307

 

                        391  g(x) e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]]

                              Detach, 387, 390

 

                        392  g(x) e pnm

                              Split, 391

 

                        393  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                        & ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                        & ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 391

 

                        394  ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]

                              Split, 393

 

                        395  ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]

                              Split, 393

 

                        396  ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]

                              Split, 393

 

                        397  ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]

                              U Spec, 395

 

                        398  ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]

                              U Spec, 397

 

                        399  (x,0) e g(x) & (x,1) e g(x) => 0=1

                              U Spec, 398

 

                        400  (x,0) e g(x) & (x,1) e g(x)

                              Join, 383, 380

 

                        401  0=1

                              Detach, 399, 400

 

                        402  ~0=1 => y1=y2

                              Arb Cons, 401

 

                        403  y1=y2

                              Detach, 402, 8

 

              As Required:

 

                  404  (x,0) e g(x) & y2=1 => y1=y2

                        4 Conclusion, 382

 

                  

                   Sub-case 2

                  

                   Prove: (x,1) e g(x) & y2=0 => y1=y2

                  

                   Suppose...

 

                        405  (x,1) e g(x) & y2=0

                              Premise

 

                        406  (x,1) e g(x)

                              Split, 405

 

                        407  y2=0

                              Split, 405

 

                        408  y1=y2

                              Substitute, 407, 381

 

              As Required:

 

                  409  (x,1) e g(x) & y2=0 => y1=y2

                        4 Conclusion, 405

 

                  

                   Sub-case 3

                  

                   Prove: (x,2) e g(x) & y2=0 => y1=y2

                  

                   Suppose...

 

                        410  (x,2) e g(x) & y2=0

                              Premise

 

                        411  (x,2) e g(x)

                              Split, 410

 

                        412  y2=0

                              Split, 410

 

                        413  y1=y2

                              Substitute, 412, 381

 

              As Required:

 

                  414  (x,2) e g(x) & y2=0 => y1=y2

                        4 Conclusion, 410

 

                  415  [(x,0) e g(x) & y2=1 => y1=y2]

                   & [(x,1) e g(x) & y2=0 => y1=y2]

                        Join, 404, 409

 

                  416  [(x,0) e g(x) & y2=1 => y1=y2]

                   & [(x,1) e g(x) & y2=0 => y1=y2]

                   & [(x,2) e g(x) & y2=0 => y1=