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=