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=y2]
Join, 415, 414
417 y1=y2
Cases, 316, 416
As Required:
418 (x,1) e g(x) & y1=0 => y1=y2
4 Conclusion, 379
Case 3
Prove: (x,2) e g(x) & y1=0 => y1=y2
Suppose...
419 (x,2) e g(x) & y1=0
Premise
420 (x,2) e g(x)
Split, 419
421 y1=0
Split, 419
Sub-case 1
Prove: (x,0) e g(x) & y2=1 => y1=y2
Suppose...
422 (x,0) e g(x) & y2=1
Premise
423 (x,0) e g(x)
Split, 422
424 y2=1
Split, 422
Apply definition of g
425 x e n => g(x) e t'
U Spec, 124
426 g(x) e t'
Detach, 425, 307
Apply definition of t'
427 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
428 [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, 427
429 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, 428
430 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, 428
431 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, 429, 426
432 g(x) e pnm
Split, 431
433 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, 431
434 ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]
Split, 433
435 ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]
Split, 433
436 ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]
Split, 433
437 ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]
U Spec, 435
438 ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]
U Spec, 437
439 (x,0) e g(x) & (x,2) e g(x) => 0=2
U Spec, 438
440 (x,0) e g(x) & (x,2) e g(x)
Join, 423, 420
441 0=2
Detach, 439, 440
442 ~0=2 => y1=y2
Arb Cons, 441
443 y1=y2
Detach, 442, 9
As Required:
444 (x,0) e g(x) & y2=1 => y1=y2
4 Conclusion, 422
Sub-case 2
445 (x,1) e g(x) & y2=0
Premise
446 (x,1) e g(x)
Split, 445
447 y2=0
Split, 445
448 y1=y2
Substitute, 447, 421
As Required:
449 (x,1) e g(x) & y2=0 => y1=y2
4 Conclusion, 445
Sub-case 3
Prove: (x,2) e g(x) & y2=0 => y1=y2
Suppose...
450 (x,2) e g(x) & y2=0
Premise
451 (x,2) e g(x)
Split, 450
452 y2=0
Split, 450
453 y1=y2
Substitute, 452, 421
As Required:
454 (x,2) e g(x) & y2=0 => y1=y2
4 Conclusion, 450
455 [(x,0) e g(x) & y2=1 => y1=y2]
& [(x,1) e g(x) & y2=0 => y1=y2]
Join, 444, 449
456 [(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, 455, 454
457 y1=y2
Cases, 316, 456
As Required:
458 (x,2) e g(x) & y1=0 => y1=y2
4 Conclusion, 419
459 [(x,0) e g(x) & y1=1 => y1=y2]
& [(x,1) e g(x) & y1=0 => y1=y2]
Join, 378, 418
460 [(x,0) e g(x) & y1=1 => y1=y2]
& [(x,1) e g(x) & y1=0 => y1=y2]
& [(x,2) e g(x) & y1=0 => y1=y2]
Join, 459, 458
461 y1=y2
Cases, 309, 460
As Required:
462 ALL(c):ALL(d1):ALL(d2):[(c,d1) e h & (c,d2) e h => d1=d2]
4 Conclusion, 291
463 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]]
Join, 163, 290
464 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]
Join, 463, 462
As Required: h is a function
465 ALL(c):ALL(d):[d=h(c) <=> (c,d) e h]
Detach, 147, 464
Prove: ALL(a):[a e n
=> [(a,0) e g(a) => h(a)=1] & [(a,1) e g(a) => h(a)=0]
& [(a,2) e g(a) => h(a)=0]]
Suppose...
466 x e n
Premise
Apply definition of g
467 x e n => g(x) e t'
U Spec, 124
468 g(x) e t'
Detach, 467, 466
Apply definition of t'
469 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
470 [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, 469
471 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, 470
472 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, 470
473 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, 471, 468
474 g(x) e pnm
Split, 473
475 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, 473
476 ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]
Split, 475
477 ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]
Split, 475
478 ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]
Split, 475
From functionality of g...
479 x e n => EXIST(d):[d e m & (x,d) e h]
U Spec, 290
480 EXIST(d):[d e m & (x,d) e h]
Detach, 479, 466
481 y e m & (x,y) e h
E Spec, 480
Define: y
482 y e m
Split, 481
483 (x,y) e h
Split, 481
Apply functionality of h
484 ALL(d):[d=h(x) <=> (x,d) e h]
U Spec, 465
485 y=h(x) <=> (x,y) e h
U Spec, 484
486 [y=h(x) => (x,y) e h] & [(x,y) e h => y=h(x)]
Iff-And, 485
487 y=h(x) => (x,y) e h
Split, 486
488 (x,y) e h => y=h(x)
Split, 486
489 y=h(x)
Detach, 488, 483
Apply definition of h
490 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
491 (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, 490
492 [(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, 491
493 (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, 492
494 (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, 492
495 (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, 493, 483
496 (x,y) e nm
Split, 495
497 (x,0) e g(x) & y=1 | (x,1) e g(x) & y=0 | (x,2) e g(x) & y=0
Split, 495
498 ~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]] | (x,2) e g(x) & y=0
DeMorgan, 497
499 ~[~~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]] & ~[(x,2) e g(x) & y=0]]
DeMorgan, 498
500 ~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0] & ~[(x,2) e g(x) & y=0]]
Rem DNeg, 499
Obtain a contradiction of the above.
Prove: ~[(x,0) e g(x) & ~y=1] (i.e. (x,0) e g(x) => y=1)
Suppose to the contrary...
501 (x,0) e g(x) & ~y=1
Premise
502 (x,0) e g(x)
Split, 501
503 ~y=1
Split, 501
Prove: ~[(x,0) e g(x) & y=1]
Suppose to the contary...
504 (x,0) e g(x) & y=1
Premise
505 (x,0) e g(x)
Split, 504
506 y=1
Split, 504
507 y=1 & ~y=1
Join, 506, 503
As Required:
508 ~[(x,0) e g(x) & y=1]
4 Conclusion, 504
Prove: ~[(x,1) e g(x) & y=0]
Suppose to the contrary...
509 (x,1) e g(x) & y=0
Premise
510 (x,1) e g(x)
Split, 509
511 y=0
Split, 509
512 (x,0) e g(x) & (x,1) e g(x)
Join, 502, 510
Apply injectivity of elements of g(x)
513 ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]
U Spec, 477
514 ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]
U Spec, 513
515 (x,0) e g(x) & (x,1) e g(x) => 0=1
U Spec, 514
516 0=1
Detach, 515, 512
517 0=1 & ~0=1
Join, 516, 8
As Required:
518 ~[(x,1) e g(x) & y=0]
4 Conclusion, 509
Prove: ~[(x,2) e g(x) & y=0]
Suppose to the contrary...
519 (x,2) e g(x) & y=0
Premise
520 (x,2) e g(x)
Split, 519
521 y=0
Split, 519
522 (x,0) e g(x) & (x,2) e g(x)
Join, 502, 520
Apply injectivity of g(x)
523 ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]
U Spec, 477
524 ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]
U Spec, 523
525 (x,0) e g(x) & (x,2) e g(x) => 0=2
U Spec, 524
526 0=2
Detach, 525, 522
527 0=2 & ~0=2
Join, 526, 9
528 ~[(x,2) e g(x) & y=0]
4 Conclusion, 519
529 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
Join, 508, 518
530 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
Join, 529, 528
531 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
& ~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0] & ~[(x,2) e g(x) & y=0]]
Join, 530, 500
As Required:
532 ~[(x,0) e g(x) & ~y=1]
4 Conclusion, 501
533 ~~[(x,0) e g(x) => ~~y=1]
Imply-And, 532
534 (x,0) e g(x) => ~~y=1
Rem DNeg, 533
As Required:
535 (x,0) e g(x) => y=1
Rem DNeg, 534
Prove: ~[(x,1) e g(x) & ~y=0] (i.e. (x,1) e g(x) => y=0)
Suppose to the contrary...
536 (x,1) e g(x) & ~y=0
Premise
537 (x,1) e g(x)
Split, 536
538 ~y=0
Split, 536
Prove: ~[(x,0) e g(x) & y=1]
Suppose...
539 (x,0) e g(x) & y=1
Premise
540 (x,0) e g(x)
Split, 539
541 y=1
Split, 539
542 (x,0) e g(x) & (x,1) e g(x)
Join, 540, 537
Apply injectivity of g(x)
543 ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]
U Spec, 477
544 ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]
U Spec, 543
545 (x,0) e g(x) & (x,1) e g(x) => 0=1
U Spec, 544
546 0=1
Detach, 545, 542
547 0=1 & ~0=1
Join, 546, 8
As Required:
548 ~[(x,0) e g(x) & y=1]
4 Conclusion, 539
Prove: ~[(x,1) e g(x) & y=0]
Suppose to the contrary...
549 (x,1) e g(x) & y=0
Premise
550 (x,1) e g(x)
Split, 549
551 y=0
Split, 549
552 y=0 & ~y=0
Join, 551, 538
As Required:
553 ~[(x,1) e g(x) & y=0]
4 Conclusion, 549
Prove: ~[(x,2) e g(x) & y=0]
Suppose to the contrary...
554 (x,2) e g(x) & y=0
Premise
555 (x,2) e g(x)
Split, 554
556 y=0
Split, 554
557 y=0 & ~y=0
Join, 556, 538
As Required:
558 ~[(x,2) e g(x) & y=0]
4 Conclusion, 554
559 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
Join, 548, 553
560 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
Join, 559, 558
561 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
& ~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0] & ~[(x,2) e g(x) & y=0]]
Join, 560, 500
As Required:
562 ~[(x,1) e g(x) & ~y=0]
4 Conclusion, 536
563 ~~[(x,1) e g(x) => ~~y=0]
Imply-And, 562
564 (x,1) e g(x) => ~~y=0
Rem DNeg, 563
As Required:
565 (x,1) e g(x) => y=0
Rem DNeg, 564
Prove: ~[(x,2) e g(x) & ~y=0] (i.e. (x,2) e g(x) => y=0)
Suppose to the contrary...
566 (x,2) e g(x) & ~y=0
Premise
567 (x,2) e g(x)
Split, 566
568 ~y=0
Split, 566
Prove: ~[(x,0) e g(x) & y=1]
Suppose to the contrary...
569 (x,0) e g(x) & y=1
Premise
570 (x,0) e g(x)
Split, 569
571 y=1
Split, 569
572 (x,0) e g(x) & (x,2) e g(x)
Join, 570, 567
573 ALL(c1):ALL(c2):[(x,c1) e g(x) & (x,c2) e g(x) => c1=c2]
U Spec, 477
574 ALL(c2):[(x,0) e g(x) & (x,c2) e g(x) => 0=c2]
U Spec, 573
575 (x,0) e g(x) & (x,2) e g(x) => 0=2
U Spec, 574
576 0=2
Detach, 575, 572
577 0=2 & ~0=2
Join, 576, 9
As Required:
578 ~[(x,0) e g(x) & y=1]
4 Conclusion, 569
Prove: ~[(x,1) e g(x) & y=0]
Suppose to the contrary...
579 (x,1) e g(x) & y=0
Premise
580 (x,1) e g(x)
Split, 579
581 y=0
Split, 579
582 y=0 & ~y=0
Join, 581, 568
As Required:
583 ~[(x,1) e g(x) & y=0]
4 Conclusion, 579
Prove: ~[(x,2) e g(x) & y=0]
Suppose to the contrary...
584 (x,2) e g(x) & y=0
Premise
585 (x,2) e g(x)
Split, 584
586 y=0
Split, 584
587 y=0 & ~y=0
Join, 586, 568
As Required:
588 ~[(x,2) e g(x) & y=0]
4 Conclusion, 584
589 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
Join, 578, 583
590 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
Join, 589, 588
591 ~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0]
& ~[(x,2) e g(x) & y=0]
& ~[~[(x,0) e g(x) & y=1] & ~[(x,1) e g(x) & y=0] & ~[(x,2) e g(x) & y=0]]
Join, 590, 500
As Required:
592 ~[(x,2) e g(x) & ~y=0]
4 Conclusion, 566
593 ~~[(x,2) e g(x) => ~~y=0]
Imply-And, 592
594 (x,2) e g(x) => ~~y=0
Rem DNeg, 593
As Required:
595 (x,2) e g(x) => y=0
Rem DNeg, 594
596 [(x,0) e g(x) => y=1] & [(x,1) e g(x) => y=0]
Join, 535, 565
597 [(x,0) e g(x) => y=1] & [(x,1) e g(x) => y=0]
& [(x,2) e g(x) => y=0]
Join, 596, 595
598 [(x,0) e g(x) => h(x)=1] & [(x,1) e g(x) => h(x)=0]
& [(x,2) e g(x) => h(x)=0]
Substitute, 489, 597
As Required:
599 ALL(a):[a e n
=> [(a,0) e g(a) => h(a)=1] & [(a,1) e g(a) => h(a)=0]
& [(a,2) e g(a) => h(a)=0]]
4 Conclusion, 466
Prove: h e t'
Apply definition of t'
600 h e t' <=> h e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e h]]
& ALL(b):ALL(c1):ALL(c2):[(b,c1) e h & (b,c2) e h => c1=c2]
& ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]]
U Spec, 20
601 [h e t' => h e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e h]]
& ALL(b):ALL(c1):ALL(c2):[(b,c1) e h & (b,c2) e h => c1=c2]
& ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]]]
& [h e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e h]]
& ALL(b):ALL(c1):ALL(c2):[(b,c1) e h & (b,c2) e h => c1=c2]
& ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]] => h e t']
Iff-And, 600
602 h e t' => h e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e h]]
& ALL(b):ALL(c1):ALL(c2):[(b,c1) e h & (b,c2) e h => c1=c2]
& ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]]
Split, 601
Sufficient: For h e t'
603 h e pnm & [ALL(b):[b e n => EXIST(c):[c e m & (b,c) e h]]
& ALL(b):ALL(c1):ALL(c2):[(b,c1) e h & (b,c2) e h => c1=c2]
& ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]] => h e t'
Split, 601
Prove: h e pnm
Apply definition of pnm
604 h e pnm <=> Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm]
U Spec, 16
605 [h e pnm => Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm]]
& [Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm] => h e pnm]
Iff-And, 604
606 h e pnm => Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm]
Split, 605
Sufficient: For h e pnm
607 Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm] => h e pnm
Split, 605
608 (x,y) e h
Premise
609 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
610 (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, 609
611 [(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, 610
612 (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, 611
613 (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, 611
614 (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, 612, 608
615 (x,y) e nm
Split, 614
616 ALL(b):ALL(c):[(b,c) e h => (b,c) e nm]
4 Conclusion, 608
617 Set'(h) & ALL(b):ALL(c):[(b,c) e h => (b,c) e nm]
Join, 142, 616
As Required:
618 h e pnm
Detach, 607, 617
Prove: ALL(b):[b e n => [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]
Suppose...
619 x e n
Premise
620 x e n
=> [(x,0) e g(x) => h(x)=1] & [(x,1) e g(x) => h(x)=0]
& [(x,2) e g(x) => h(x)=0]
U Spec, 599
621 [(x,0) e g(x) => h(x)=1] & [(x,1) e g(x) => h(x)=0]
& [(x,2) e g(x) => h(x)=0]
Detach, 620, 619
622 (x,0) e g(x) => h(x)=1
Split, 621
623 (x,1) e g(x) => h(x)=0
Split, 621
624 (x,2) e g(x) => h(x)=0
Split, 621
Apply definition of g
625 x e n => g(x) e t'
U Spec, 124
626 g(x) e t'
Detach, 625, 619
Apply definition of t'
627 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
628 [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, 627
629 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, 628
630 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, 628
631 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, 629, 626
632 g(x) e pnm
Split, 631
633 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, 631
634 ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]
Split, 633
635 ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]
Split, 633
636 ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]
Split, 633
Apply definiton of pnm
637 g(x) e pnm <=> Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
U Spec, 16
638 [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, 637
639 [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, 637
640 g(x) e pnm => Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Split, 639
641 Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm] => g(x) e pnm
Split, 639
642 Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Detach, 640, 632
643 Set'(g(x))
Split, 642
644 ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Split, 642
Prove: ALL(b):[(x,b) e g(x) => b=0 | b=1 | b=2]
Suppose...
645 (x,y) e g(x)
Premise
646 ALL(c):[(x,c) e g(x) => (x,c) e nm]
U Spec, 644
647 (x,y) e g(x) => (x,y) e nm
U Spec, 646
648 (x,y) e nm
Detach, 647, 645
649 ALL(b):[(x,b) e nm <=> x e n & b e m]
U Spec, 14
650 (x,y) e nm <=> x e n & y e m
U Spec, 649
651 [(x,y) e nm => x e n & y e m]
& [x e n & y e m => (x,y) e nm]
Iff-And, 650
652 (x,y) e nm => x e n & y e m
Split, 651
653 x e n & y e m => (x,y) e nm
Split, 651
654 x e n & y e m
Detach, 652, 648
655 x e n
Split, 654
656 y e m
Split, 654
657 y e m <=> y=0 | y=1 | y=2
U Spec, 12
658 [y e m => y=0 | y=1 | y=2] & [y=0 | y=1 | y=2 => y e m]
Iff-And, 657
659 y e m => y=0 | y=1 | y=2
Split, 658
660 y=0 | y=1 | y=2 => y e m
Split, 658
661 y=0 | y=1 | y=2
Detach, 659, 656
As Required:
662 ALL(b):[(x,b) e g(x) => b=0 | b=1 | b=2]
4 Conclusion, 645
663 x e n => EXIST(c):[c e m & (x,c) e g(x)]
U Spec, 634
664 EXIST(c):[c e m & (x,c) e g(x)]
Detach, 663, 619
665 y e m & (x,y) e g(x)
E Spec, 664
666 y e m
Split, 665
667 (x,y) e g(x)
Split, 665
668 (x,y) e g(x) => y=0 | y=1 | y=2
U Spec, 662
Three cases to consider:
669 y=0 | y=1 | y=2
Detach, 668, 667
Case 1
Prove: y=0 => ~h(x)=2
Suppose...
670 y=0
Premise
671 (x,0) e g(x)
Substitute, 670, 667
672 h(x)=1
Detach, 622, 671
673 ~h(x)=2
Substitute, 672, 10
As Required:
674 y=0 => ~h(x)=2
4 Conclusion, 670
Case 2
Prove: y=1 => ~h(x)=2
Suppose...
675 y=1
Premise
676 (x,1) e g(x)
Substitute, 675, 667
677 h(x)=0
Detach, 623, 676
678 ~h(x)=2
Substitute, 677, 9
As Required:
679 y=1 => ~h(x)=2
4 Conclusion, 675
Case 3
Define: y=2 => ~h(x)=2
Suppose...
680 y=2
Premise
681 (x,2) e g(x)
Substitute, 680, 667
682 h(x)=0
Detach, 624, 681
683 ~h(x)=2
Substitute, 682, 9
As Required:
684 y=2 => ~h(x)=2
4 Conclusion, 680
685 [y=0 => ~h(x)=2] & [y=1 => ~h(x)=2]
Join, 674, 679
686 [y=0 => ~h(x)=2] & [y=1 => ~h(x)=2]
& [y=2 => ~h(x)=2]
Join, 685, 684
* Line 763
687 ~h(x)=2
Cases, 669, 686
688 ALL(d):[d=h(x) <=> (x,d) e h]
U Spec, 465
689 2=h(x) <=> (x,2) e h
U Spec, 688
690 [2=h(x) => (x,2) e h] & [(x,2) e h => 2=h(x)]
Iff-And, 689
691 2=h(x) => (x,2) e h
Split, 690
692 (x,2) e h => 2=h(x)
Split, 690
693 ~2=h(x) => ~(x,2) e h
Contra, 692
694 ~h(x)=2 => ~(x,2) e h
Sym, 693
695 ~(x,2) e h
Detach, 694, 687
696 ~~(x,2) e h => EXIST(c):[c e n & [x<c & ~(c,2) e h]]
Arb Cons, 695
697 (x,2) e h => EXIST(c):[c e n & [x<c & ~(c,2) e h]]
Rem DNeg, 696
As Required:
698 ALL(b):[b e n
=> [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]
4 Conclusion, 619
699 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]
Join, 290, 462
700 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(b):[b e n
=> [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]
Join, 699, 698
701 h e pnm
& [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(b):[b e n
=> [(b,2) e h => EXIST(c):[c e n & [b<c & ~(c,2) e h]]]]]
Join, 618, 700
As Required:
702 h e t'
Detach, 603, 701
Prove: ALL(d):[d e n => ~g(d)=h] (i.e. string h is not in the range of function g)
Suppose...
703 x e n
Premise
704 x e n => g(x) e t'
U Spec, 124
705 g(x) e t'
Detach, 704, 703
Apply the definition of t'
706 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
707 [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, 706
708 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, 707
709 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, 707
710 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, 708, 705
711 g(x) e pnm
Split, 710
712 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, 710
713 ALL(b):[b e n => EXIST(c):[c e m & (b,c) e g(x)]]
Split, 712
714 ALL(b):ALL(c1):ALL(c2):[(b,c1) e g(x) & (b,c2) e g(x) => c1=c2]
Split, 712
715 ALL(b):[b e n => [(b,2) e g(x) => EXIST(c):[c e n & [b<c & ~(c,2) e g(x)]]]]
Split, 712
716 g(x) e pnm <=> Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
U Spec, 16
717 [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, 716
718 g(x) e pnm => Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Split, 717
719 Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm] => g(x) e pnm
Split, 717
720 Set'(g(x)) & ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Detach, 718, 711
721 Set'(g(x))
Split, 720
722 ALL(b):ALL(c):[(b,c) e g(x) => (b,c) e nm]
Split, 720
723 ALL(a):ALL(b):[Set'(a) & Set'(b) => [a=b
<=> ALL(c1):ALL(c2):[(c1,c2) e a <=> (c1,c2) e b]]]
Set Equality
724 ALL(b):[Set'(g(x)) & Set'(b) => [g(x)=b
<=> ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e b]]]
U Spec, 723
725 Set'(g(x)) & Set'(h) => [g(x)=h
<=> ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h]]
U Spec, 724
726 Set'(g(x)) & Set'(h)
Join, 721, 142
727 g(x)=h
<=> ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h]
Detach, 725, 726
728 [g(x)=h => ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h]]
& [ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h] => g(x)=h]
Iff-And, 727
729 g(x)=h => ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h]
Split, 728
730 ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h] => g(x)=h
Split, 728
731 ~ALL(c1):ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h] => ~g(x)=h
Contra, 729
732 ~~EXIST(c1):~ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h] => ~g(x)=h
Quant, 731
733 EXIST(c1):~ALL(c2):[(c1,c2) e g(x) <=> (c1,c2) e h] => ~g(x)=h
Rem DNeg, 732
734 EXIST(c1):~~EXIST(c2):~[(c1,c2) e g(x) <=> (c1,c2) e h] => ~g(x)=h
Quant, 733
735 EXIST(c1):EXIST(c2):~[(c1,c2) e g(x) <=> (c1,c2) e h] => ~g(x)=h
Rem DNeg, 734
736 EXIST(c1):EXIST(c2):~[[(c1,c2) e g(x) => (c1,c2) e h]
& [(c1,c2) e h => (c1,c2) e g(x)]] => ~g(x)=h
Iff-And, 735
737 EXIST(c1):EXIST(c2):~~[~[(c1,c2) e g(x) => (c1,c2) e h] | ~[(c1,c2) e h => (c1,c2) e g(x)]] => ~g(x)=h
DeMorgan, 736
738 EXIST(c1):EXIST(c2):[~[(c1,c2) e g(x) => (c1,c2) e h] | ~[(c1,c2) e h => (c1,c2) e g(x)]] => ~g(x)=h
Rem DNeg, 737
739 EXIST(c1):EXIST(c2):[~~[(c1,c2) e g(x) & ~(c1,c2) e h] | ~[(c1,c2) e h => (c1,c2) e g(x)]] => ~g(x)=h
Imply-And, 738
740 EXIST(c1):EXIST(c2):[(c1,c2) e g(x) & ~(c1,c2) e h | ~[(c1,c2) e h => (c1,c2) e g(x)]] => ~g(x)=h
Rem DNeg, 739
741 EXIST(c1):EXIST(c2):[(c1,c2) e g(x) & ~(c1,c2) e h | ~~[(c1,c2) e h & ~(c1,c2) e g(x)]] => ~g(x)=h
Imply-And, 740
Sufficient: For ~g(x)=h
742 EXIST(c1):EXIST(c2):[(c1,c2) e g(x) & ~(c1,c2) e h | (c1,c2) e h & ~(c1,c2) e g(x)] => ~g(x)=h
Rem DNeg, 741
743 x e n => EXIST(c):[c e m & (x,c) e g(x)]
U Spec, 713
744 EXIST(c):[c e m & (x,c) e g(x)]
Detach, 743, 703
745 y e m & (x,y) e g(x)
E Spec, 744
Define: y
746 y e m
Split, 745
747 (x,y) e g(x)
Split, 745
748 y e m <=> y=0 | y=1 | y=2
U Spec, 12
749 [y e m => y=0 | y=1 | y=2] & [y=0 | y=1 | y=2 => y e m]
Iff-And, 748
750 y e m => y=0 | y=1 | y=2
Split, 749
751 y=0 | y=1 | y=2 => y e m
Split, 749
Three cases to consider:
752 y=0 | y=1 | y=2
Detach, 750, 746
753 x e n
=> [(x,0) e g(x) => h(x)=1] & [(x,1) e g(x) => h(x)=0]
& [(x,2) e g(x) => h(x)=0]
U Spec, 599
754 [(x,0) e g(x) => h(x)=1] & [(x,1) e g(x) => h(x)=0]
& [(x,2) e g(x) => h(x)=0]
Detach, 753, 703
755 (x,0) e g(x) => h(x)=1
Split, 754
756 (x,1) e g(x) => h(x)=0
Split, 754
757 (x,2) e g(x) => h(x)=0
Split, 754
758 y=0
Premise
759 (x,0) e g(x)
Substitute, 758, 747
760 h(x)=1
Detach, 755, 759
761 ~y=1
Substitute, 758, 8
762 ~y=h(x)
Substitute, 760, 761
763 ~h(x)=y
Sym, 762
764 y=0 => ~h(x)=y
4 Conclusion, 758
765 y=1
Premise
766 (x,1) e g(x)
Substitute, 765, 747
767 h(x)=0
Detach, 756, 766
768 ~0=y
Substitute, 765, 8
769 ~h(x)=y
Substitute, 767, 768
770 y=1 => ~h(x)=y
4 Conclusion, 765
771 y=2
Premise
772 (x,2) e g(x)
Substitute, 771, 747
773 h(x)=0
Detach, 757, 772
774 ~0=y
Substitute, 771, 9
775 ~h(x)=y
Substitute, 773, 774
776 y=2 => ~h(x)=y
4 Conclusion, 771
777 [y=0 => ~h(x)=y] & [y=1 => ~h(x)=y]
Join, 764, 770
778 [y=0 => ~h(x)=y] & [y=1 => ~h(x)=y]
& [y=2 => ~h(x)=y]
Join, 777, 776
779 ~h(x)=y
Cases, 752, 778
780 ALL(d):[d=h(x) <=> (x,d) e h]
U Spec, 465
781 y=h(x) <=> (x,y) e h
U Spec, 780
782 [y=h(x) => (x,y) e h] & [(x,y) e h => y=h(x)]
Iff-And, 781
783 y=h(x) => (x,y) e h
Split, 782
784 (x,y) e h => y=h(x)
Split, 782
785 ~y=h(x) => ~(x,y) e h
Contra, 784
786 ~h(x)=y => ~(x,y) e h
Sym, 785
787 ~(x,y) e h
Detach, 786, 779
788 (x,y) e g(x) & ~(x,y) e h
Join, 747, 787
789 (x,y) e g(x) & ~(x,y) e h | (x,y) e h & ~(x,y) e g(x)
Arb Or, 788
790 EXIST(c2):[(x,c2) e g(x) & ~(x,c2) e h | (x,c2) e h & ~(x,c2) e g(x)]
E Gen, 789
791 EXIST(c1):EXIST(c2):[(c1,c2) e g(x) & ~(c1,c2) e h | (c1,c2) e h & ~(c1,c2) e g(x)]
E Gen, 790
792 ~g(x)=h
Detach, 742, 791
As Required:
793 ALL(d):[d e n => ~g(d)=h]
4 Conclusion, 703
794 h e t' & ALL(d):[d e n => ~g(d)=h]
Join, 702, 793
795 EXIST(c):[c e t' & ALL(d):[d e n => ~g(d)=c]]
E Gen, 794
796 ~Surjection(g,n,t')
Detach, 139, 795
As Required:
797 ALL(g):[ALL(a):[a e n => g(a) e t'] => ~Surjection(g,n,t')]
4 Conclusion, 124
As Required:
798 ~Countable(t')
Detach, 123, 797