THEOREM
*******
Given a function f mapping set x to set y, there exists an
INJECTIVE function h mapping the range of f back to the set x.
ALL(x):ALL(y):[Set(x)
& Set(y)
=> ALL(f):[ALL(a):[a
e x => f(a) e y]
=>
EXIST(h):[ALL(a):[a e y & EXIST(b):[b e x & f(b)=a] => h(a) e x]
& ALL(a):ALL(b):[a e y & b e y
& EXIST(c):[c e x & f(c)=a] & EXIST(d):[d e x & f(d)=b] => [h(a)=h(b) => a=b]]]]]
This proof makes use of the DC Prof Axiom of Choice:
ALL(f):[Set(f) &
ALL(a):[a e f => Set(a) & EXIST(b):b e a] =>
EXIST(c):ALL(a):[a e f => c(a) e a]] (line 285)
This proof was written and verified with the aid of the author's
DC Proof 2.0 freeware available at http://www.dcproof.com
Dan Christensen
2020-12-07
OUTLINE
*******
Construct function g that maps each element of the range of f to
the set of the pre-images
of that element. Then construct a choice function to select a
single element from each of those sets. Then compose the
these functions to get h(t) = choice(g(f(t))) for all t in x.
Finally, prove that h is injective.
PROOF
*****
Suppose...
1 Set(x) & Set(y)
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
Define: f (function)
4 ALL(a):[a e x => f(a) e y]
Premise
Construct range of
f
Apply Subset Axiom
5 EXIST(a):[Set(a)
& ALL(b):[b e a <=> b e y & EXIST(c):[c e x & f(c)=b]]]
Subset, 3
6 Set(rf) & ALL(b):[b e rf <=> b e y & EXIST(c):[c e x & f(c)=b]]
E Spec, 5
Define: rf (range of f)
7 Set(rf)
Split, 6
8 ALL(b):[b e rf <=> b e y & EXIST(c):[c e x & f(c)=b]]
Split, 6
Construct the
function g that maps each element of the range of f to the set of its
pre-images in set x
Apply Power Set
Axiom
9 ALL(a):[Set(a)
=> EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e a]]]]
Power Set
10 Set(x) =>
EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e x]]]
U Spec, 9
11 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set(c) & ALL(d):[d e c => d e x]]]
Detach, 10, 2
12 Set(px)
& ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
E Spec, 11
Define: px (power set of x)
13 Set(px)
Split, 12
14 ALL(c):[c e px <=> Set(c) & ALL(d):[d e c => d e x]]
Split, 12
Construct
Cartesian product of rf x px
Apply Cartesian
Product Axiom
15 ALL(a1):ALL(a2):[Set(a1)
& Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
16 ALL(a2):[Set(rf) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e a2]]]
U Spec, 15
17 Set(rf) & Set(px) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e px]]
U Spec, 16
18 Set(rf) & Set(px)
Join, 7, 13
19 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e px]]
Detach, 17, 18
20 Set'(rfpx) &
ALL(c1):ALL(c2):[(c1,c2) e rfpx <=> c1 e rf & c2 e px]
E Spec, 19
Define: rfpx (rf x px)
21 Set'(rfpx)
Split, 20
22 ALL(c1):ALL(c2):[(c1,c2) e rfpx <=> c1 e rf & c2 e px]
Split, 20
Construct subset
of rfpx
Apply Subset Axiom
23 EXIST(a):[Set'(a)
& ALL(b):ALL(c):[(b,c) e a <=>
(b,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=b]]]]
Subset, 21
24 Set'(g) &
ALL(b):ALL(c):[(b,c) e g <=> (b,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=b]]]
E Spec, 23
Define: g (as a subset of rfpx)
25 Set'(g)
Split, 24
26 ALL(b):ALL(c):[(b,c) e g <=> (b,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=b]]]
Split, 24
Apply Function
Axiom
27 ALL(f):ALL(dom):ALL(cod):[Set'(f)
& Set(dom) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=> [(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e dom & b e cod => [f(a1)=b <=> (a1,b) e f]]]]
Function
28 ALL(dom):ALL(cod):[Set'(g) & Set(dom)
& Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=> ALL(a1):ALL(b):[a1 e dom & b e cod => [g(a1)=b <=>
(a1,b) e g]]]]
U Spec, 27
29 ALL(cod):[Set'(g) & Set(rf) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e cod]
&
ALL(a1):[a1 e rf => EXIST(b):[b e cod & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e cod & b2 e cod
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e cod => [g(a1)=b <=>
(a1,b) e g]]]]
U Spec, 28
30 Set'(g) & Set(rf) & Set(px)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
&
ALL(a1):[a1 e rf => EXIST(b):[b e px & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e px & b2 e px
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e px => [g(a1)=b <=>
(a1,b) e g]]]
U Spec, 29
31 Set'(g) & Set(rf)
Join, 25, 7
32 Set'(g) & Set(rf) & Set(px)
Join, 31, 13
Sufficient: For
functionality of g
33 ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
&
ALL(a1):[a1 e rf => EXIST(b):[b e px & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e px & b2 e px
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e px => [g(a1)=b <=>
(a1,b) e g]]
Detach, 30, 32
Step 1
Prove:
ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
Suppose...
34 (t,u) e g
Premise
35 ALL(c):[(t,c) e g <=> (t,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=t]]]
U Spec, 26
36 (t,u) e g <=> (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
U Spec, 35
37 [(t,u) e g => (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]]
& [(t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]] => (t,u) e g]
Iff-And, 36
38 (t,u) e g => (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
Split, 37
39 (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]] => (t,u) e g
Split, 37
40 (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
Detach, 38, 34
41 (t,u) e rfpx
Split, 40
42 ALL(d):[d e x => [d e u <=> f(d)=t]]
Split, 40
43 ALL(c2):[(t,c2) e rfpx <=> t e rf & c2 e px]
U Spec, 22
44 (t,u) e rfpx <=> t e rf & u e px
U Spec, 43
45 [(t,u) e rfpx => t e rf & u e px]
& [t e rf & u e px => (t,u) e rfpx]
Iff-And, 44
46 (t,u) e rfpx => t e rf & u e px
Split, 45
47 t e rf & u e px => (t,u) e rfpx
Split, 45
48 t e rf & u e px
Detach, 46, 41
As Required:
49 ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
4 Conclusion, 34
Step 2
Prove:
ALL(a1):[a1 e rf => EXIST(b):[b e px &
(a1,b) e g]]
Suppose...
50 t e rf
Premise
51 EXIST(a):[Set(a)
& ALL(b):[b e a <=> b e x & f(b)=t]]
Subset, 2
52 Set(gt) &
ALL(b):[b e gt <=> b e x & f(b)=t]
E Spec, 51
Define: gt
53 Set(gt)
Split, 52
54 ALL(b):[b e gt <=> b e x & f(b)=t]
Split, 52
55 gt e px <=> Set(gt) & ALL(d):[d e gt => d e x]
U Spec, 14
56 [gt e px => Set(gt) & ALL(d):[d e gt => d e x]]
& [Set(gt) &
ALL(d):[d e gt => d e x] => gt e px]
Iff-And, 55
57 gt e px => Set(gt) & ALL(d):[d e gt => d e x]
Split, 56
Sufficient:
For gt e px
58 Set(gt) &
ALL(d):[d e gt => d e x] => gt e px
Split, 56
Prove:
ALL(d):[d e gt => d e x]
Suppose...
59 u e gt
Premise
60 u e gt <=> u e x & f(u)=t
U Spec, 54
61 [u e gt => u e x & f(u)=t] & [u e x & f(u)=t => u e gt]
Iff-And, 60
62 u e gt => u e x & f(u)=t
Split, 61
63 u e x & f(u)=t => u e gt
Split, 61
64 u e x & f(u)=t
Detach, 62, 59
65 u e x
Split, 64
As Required:
66 ALL(d):[d e gt => d e x]
4 Conclusion, 59
67 Set(gt) &
ALL(d):[d e gt => d e x]
Join, 53, 66
68 gt e px
Detach, 58, 67
69 ALL(c):[(t,c) e g <=> (t,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=t]]]
U Spec, 26
70 (t,gt) e g <=> (t,gt) e rfpx & ALL(d):[d e x => [d e gt <=> f(d)=t]]
U Spec, 69
71 [(t,gt) e g => (t,gt) e rfpx & ALL(d):[d e x => [d e gt <=> f(d)=t]]]
& [(t,gt) e rfpx & ALL(d):[d e x => [d e gt <=> f(d)=t]] => (t,gt) e g]
Iff-And, 70
72 (t,gt) e g => (t,gt) e rfpx & ALL(d):[d e x => [d e gt <=> f(d)=t]]
Split, 71
Sufficient:
For (t,gt) e g
73 (t,gt) e rfpx & ALL(d):[d e x => [d e gt <=> f(d)=t]] => (t,gt) e g
Split, 71
74 ALL(c2):[(t,c2) e rfpx <=> t e rf & c2 e px]
U Spec, 22
75 (t,gt) e rfpx <=> t e rf & gt e px
U Spec, 74
76 [(t,gt) e rfpx => t e rf & gt e px]
& [t e rf & gt e px => (t,gt) e rfpx]
Iff-And, 75
77 (t,gt) e rfpx => t e rf & gt e px
Split, 76
78 t e rf & gt e px => (t,gt) e rfpx
Split, 76
79 t e rf & gt e px
Join, 50, 68
80 (t,gt) e rfpx
Detach, 78, 79
Prove:
ALL(d):[d e x => [d e gt <=>
f(d)=t]]
Suppose...
81 u e x
Premise
82 u e gt <=> u e x & f(u)=t
U Spec, 54
83 [u e gt => u e x & f(u)=t] & [u e x & f(u)=t => u e gt]
Iff-And, 82
84 u e gt => u e x & f(u)=t
Split, 83
85 u e x & f(u)=t => u e gt
Split, 83
Prove:
u e gt => f(u)=t
Suppose...
86 u e gt
Premise
87 u e x & f(u)=t
Detach, 84, 86
88 u e x
Split, 87
89 f(u)=t
Split, 87
As
Required:
90 u e gt => f(u)=t
4 Conclusion, 86
Prove:
f(u)=t => u e gt
Suppose...
91 f(u)=t
Premise
92 u e x & f(u)=t
Join, 81, 91
93 u e gt
Detach, 85, 92
As
Required:
94 f(u)=t => u e gt
4 Conclusion, 91
95 [u e gt => f(u)=t] & [f(u)=t => u e gt]
Join, 90, 94
96 u e gt <=> f(u)=t
Iff-And, 95
As Required:
97 ALL(d):[d e x => [d e gt <=> f(d)=t]]
4 Conclusion, 81
98 (t,gt) e rfpx
&
ALL(d):[d e x => [d e gt <=> f(d)=t]]
Join, 80, 97
99 (t,gt) e g
Detach, 73, 98
100 gt e px & (t,gt) e g
Join, 68, 99
As Required:
101 ALL(a1):[a1 e rf => EXIST(b):[b e px & (a1,b) e g]]
4 Conclusion, 50
Step 3
Prove:
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e px & b2 e px
=> [(a1,b1) e g & (a1,b2) e g =>
b1=b2]]
Suppose...
102 t e rf & u1 e px & u2 e px
Premise
103 t e rf
Split, 102
104 u1 e px
Split, 102
105 u2 e px
Split, 102
Prove:
(t,u1) e g & (t,u2) e g => u1=u2
Suppose...
106 (t,u1) e g & (t,u2) e g
Premise
107 (t,u1) e g
Split, 106
108 (t,u2) e g
Split, 106
109 ALL(c):[(t,c) e g <=> (t,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=t]]]
U Spec, 26
110 (t,u1) e g <=> (t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]]
U Spec, 109
111 [(t,u1) e g => (t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]]]
&
[(t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]] => (t,u1) e g]
Iff-And, 110
112 (t,u1) e g => (t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]]
Split, 111
113 (t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]] => (t,u1) e g
Split, 111
114 (t,u1) e rfpx & ALL(d):[d e x => [d e u1 <=> f(d)=t]]
Detach, 112, 107
115 (t,u1) e rfpx
Split, 114
116 ALL(d):[d e x => [d e u1 <=> f(d)=t]]
Split, 114
117 (t,u2) e g <=> (t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]]
U Spec, 109
118 [(t,u2) e g => (t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]]]
&
[(t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]] => (t,u2) e g]
Iff-And, 117
119 (t,u2) e g => (t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]]
Split, 118
120 (t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]] => (t,u2) e g
Split, 118
121 (t,u2) e rfpx & ALL(d):[d e x => [d e u2 <=> f(d)=t]]
Detach, 119, 108
122 (t,u2) e rfpx
Split, 121
123 ALL(d):[d e x => [d e u2 <=> f(d)=t]]
Split, 121
124 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
125 ALL(b):[Set(u1) & Set(b) => [u1=b <=> ALL(c):[c e u1 <=> c e b]]]
U Spec, 124
126 Set(u1) & Set(u2) => [u1=u2 <=> ALL(c):[c e u1 <=> c e u2]]
U Spec, 125
127 u1 e px <=> Set(u1) &
ALL(d):[d e u1 => d e x]
U Spec, 14
128 [u1 e px => Set(u1) &
ALL(d):[d e u1 => d e x]]
&
[Set(u1) &
ALL(d):[d e u1 => d e x] => u1 e px]
Iff-And, 127
129 u1 e px => Set(u1) &
ALL(d):[d e u1 => d e x]
Split, 128
130 Set(u1) & ALL(d):[d e u1 => d e x] => u1 e px
Split, 128
131 Set(u1) & ALL(d):[d e u1 => d e x]
Detach, 129, 104
132 Set(u1)
Split, 131
133 ALL(d):[d e u1 => d e x]
Split, 131
134 u2 e px <=> Set(u2) &
ALL(d):[d e u2 => d e x]
U Spec, 14
135 [u2 e px => Set(u2) &
ALL(d):[d e u2 => d e x]]
&
[Set(u2) &
ALL(d):[d e u2 => d e x] => u2 e px]
Iff-And, 134
136 u2 e px => Set(u2) &
ALL(d):[d e u2 => d e x]
Split, 135
137 Set(u2) & ALL(d):[d e u2 => d e x] => u2 e px
Split, 135
138 Set(u2) & ALL(d):[d e u2 => d e x]
Detach, 136, 105
139 Set(u2)
Split, 138
140 ALL(d):[d e u2 => d e x]
Split, 138
141 Set(u1) & Set(u2)
Join, 132, 139
142 u1=u2 <=> ALL(c):[c e u1 <=> c e u2]
Detach, 126, 141
143 [u1=u2 => ALL(c):[c e u1 <=> c e u2]]
&
[ALL(c):[c e u1 <=> c e u2] => u1=u2]
Iff-And, 142
144 u1=u2 => ALL(c):[c e u1 <=> c e u2]
Split, 143
Sufficient:
For u1=u2
145 ALL(c):[c e u1 <=> c e u2] => u1=u2
Split, 143
'=>'
Prove:
ALL(c):[c e u1 => c e u2]
Suppose...
146 v e u1
Premise
147 v e x => [v e u1 <=> f(v)=t]
U Spec, 116
148 v e u1 => v e x
U Spec, 133
149 v e x
Detach, 148, 146
150 v e u1 <=> f(v)=t
Detach, 147, 149
151 [v e u1 => f(v)=t] & [f(v)=t => v e u1]
Iff-And, 150
152 v e u1 => f(v)=t
Split, 151
153 f(v)=t => v e u1
Split, 151
154 f(v)=t
Detach, 152, 146
155 v e x => [v e u2 <=> f(v)=t]
U Spec, 123
156 v e u2 <=> f(v)=t
Detach, 155, 149
157 [v e u2 => f(v)=t] & [f(v)=t => v e u2]
Iff-And, 156
158 v e u2 => f(v)=t
Split, 157
159 f(v)=t => v e u2
Split, 157
160 v e u2
Detach, 159, 154
As
Required:
161 ALL(c):[c e u1 => c e u2]
4 Conclusion, 146
'<='
Prove:
ALL(c):[c e u2 => c e u1]
Suppose...
162 v e u2
Premise
163 v e x => [v e u2 <=> f(v)=t]
U Spec, 123
164 v e u2 => v e x
U Spec, 140
165 v e x
Detach, 164, 162
166 v e u2 <=> f(v)=t
Detach, 163, 165
167 [v e u2 => f(v)=t] & [f(v)=t => v e u2]
Iff-And, 166
168 v e u2 => f(v)=t
Split, 167
169 f(v)=t => v e u2
Split, 167
170 f(v)=t
Detach, 168, 162
171 v e x => [v e u1 <=> f(v)=t]
U Spec, 116
172 v e u1 <=> f(v)=t
Detach, 171, 165
173 [v e u1 => f(v)=t] & [f(v)=t => v e u1]
Iff-And, 172
174 v e u1 => f(v)=t
Split, 173
175 f(v)=t => v e u1
Split, 173
176 v e u1
Detach, 175, 170
As
Required:
177 ALL(c):[c e u2 => c e u1]
4 Conclusion, 162
178 ALL(c):[[c e u1 => c e u2] & [c e u2 => c e u1]]
Join, 161, 177
179 ALL(c):[c e u1 <=> c e u2]
Iff-And, 178
180 u1=u2
Detach, 145, 179
As Required:
181 (t,u1) e g & (t,u2) e g => u1=u2
4 Conclusion, 106
As Required:
182 ALL(a):ALL(b1):ALL(b2):[a e rf & b1 e px & b2 e px
=> [(a,b1) e g & (a,b2) e g => b1=b2]]
4 Conclusion, 102
183 ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
&
ALL(a1):[a1 e rf => EXIST(b):[b e px & (a1,b) e g]]
Join, 49, 101
184 ALL(a1):ALL(b):[(a1,b) e g => a1 e rf & b e px]
&
ALL(a1):[a1 e rf => EXIST(b):[b e px & (a1,b) e g]]
&
ALL(a):ALL(b1):ALL(b2):[a e rf & b1 e px & b2 e px
=> [(a,b1) e g & (a,b2) e g => b1=b2]]
Join, 183, 182
g is a function
As Required:
185 ALL(a1):ALL(b):[a1 e rf & b e px => [g(a1)=b <=> (a1,b) e g]]
Detach, 33, 184
Prove:
ALL(a):[a e rf => g(a) e px]
Suppose...
186 t e rf
Premise
187 t e rf => EXIST(b):[b e px & (t,b) e g]
U Spec, 101
188 EXIST(b):[b e px & (t,b) e g]
Detach, 187, 186
189 u e px & (t,u) e g
E Spec, 188
190 u e px
Split, 189
191 (t,u) e g
Split, 189
192 ALL(b):[t e rf & b e px => [g(t)=b <=> (t,b) e g]]
U Spec, 185
193 t e rf & u e px => [g(t)=u <=> (t,u) e g]
U Spec, 192
194 t e rf & u e px
Join, 186, 190
195 g(t)=u <=> (t,u) e g
Detach, 193, 194
196 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 195
197 g(t)=u => (t,u) e g
Split, 196
198 (t,u) e g => g(t)=u
Split, 196
199 g(t)=u
Detach, 198, 191
200 g(t) e px
Substitute, 199,
190
Redefine g:
201 ALL(a):[a e rf => g(a) e px]
4 Conclusion, 186
Prove:
ALL(a):[a e rf => ALL(d):[d e x => [d e g(a) <=> f(d)=a]]]
Suppose...
202 t e rf
Premise
203 t e rf => EXIST(b):[b e px & (t,b) e g]
U Spec, 101
204 EXIST(b):[b e px & (t,b) e g]
Detach, 203, 202
205 u e px & (t,u) e g
E Spec, 204
206 u e px
Split, 205
207 (t,u) e g
Split, 205
208 ALL(c):[(t,c) e g <=> (t,c) e rfpx & ALL(d):[d e x => [d e c <=> f(d)=t]]]
U Spec, 26
209 (t,u) e g <=> (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
U Spec, 208
210 [(t,u) e g => (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]]
& [(t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]] => (t,u) e g]
Iff-And, 209
211 (t,u) e g => (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
Split, 210
212 (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]] => (t,u) e g
Split, 210
213 (t,u) e rfpx & ALL(d):[d e x => [d e u <=> f(d)=t]]
Detach, 211, 207
214 (t,u) e rfpx
Split, 213
215 ALL(d):[d e x => [d e u <=> f(d)=t]]
Split, 213
216 ALL(b):[t e rf & b e px => [g(t)=b <=> (t,b) e g]]
U Spec, 185
217 t e rf & u e px => [g(t)=u <=> (t,u) e g]
U Spec, 216
218 t e rf & u e px
Join, 202, 206
219 g(t)=u <=> (t,u) e g
Detach, 217, 218
220 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 219
221 g(t)=u => (t,u) e g
Split, 220
222 (t,u) e g => g(t)=u
Split, 220
223 g(t)=u
Detach, 222, 207
224 ALL(d):[d e x => [d e g(t) <=> f(d)=t]]
Substitute, 223,
215
As Required:
225 ALL(a):[a e rf => ALL(d):[d e x => [d e g(a) <=> f(d)=a]]]
4 Conclusion, 202
Prove:
ALL(a):[a e x => a e g(f(a))]
Suppose...
226 t e x
Premise
227 t e x => f(t) e y
U Spec, 4
228 f(t) e y
Detach, 227, 226
229 f(t) e rf <=> f(t) e y & EXIST(c):[c e x & f(c)=f(t)]
U Spec, 8, 228
230 [f(t) e rf => f(t) e y & EXIST(c):[c e x & f(c)=f(t)]]
& [f(t) e y & EXIST(c):[c e x & f(c)=f(t)] => f(t) e rf]
Iff-And, 229
231 f(t) e rf => f(t) e y & EXIST(c):[c e x & f(c)=f(t)]
Split, 230
232 f(t) e y & EXIST(c):[c e x & f(c)=f(t)] => f(t) e rf
Split, 230
233 f(t)=f(t)
Reflex, 228
234 t e x & f(t)=f(t)
Join, 226, 233
235 EXIST(c):[c e x & f(c)=f(t)]
E Gen, 234
236 f(t) e y & EXIST(c):[c e x & f(c)=f(t)]
Join, 228, 235
237 f(t) e rf
Detach, 232, 236
238 f(t) e rf => ALL(d):[d e x => [d e g(f(t)) <=> f(d)=f(t)]]
U Spec, 225, 237
239 ALL(d):[d e x => [d e g(f(t)) <=> f(d)=f(t)]]
Detach, 238, 237
240 t e x => [t e g(f(t)) <=> f(t)=f(t)]
U Spec, 239
241 t e g(f(t)) <=> f(t)=f(t)
Detach, 240, 226
242 [t e g(f(t)) => f(t)=f(t)] & [f(t)=f(t) => t e g(f(t))]
Iff-And, 241
243 t e g(f(t)) => f(t)=f(t)
Split, 242
244 f(t)=f(t) => t e g(f(t))
Split, 242
245 f(t)=f(t)
Reflex, 237
246 t e g(f(t))
Detach, 244, 245
As Required:
247 ALL(a):[a e x => a e g(f(a))]
4 Conclusion, 226
Construct the
range of g
248 EXIST(a):[Set(a)
& ALL(b):[b e a <=> b e px & EXIST(c):[c e rf & b=g(c)]]]
Subset, 13
249 Set(rg) &
ALL(b):[b e rg <=> b e px & EXIST(c):[c e rf & b=g(c)]]
E Spec, 248
Define: rg (range of g)
250 Set(rg)
Split, 249
251 ALL(b):[b e rg <=> b e px & EXIST(c):[c e rf & b=g(c)]]
Split, 249
Suppose...
252 t e rg
Premise
253 t e rg <=> t e px & EXIST(c):[c e rf & t=g(c)]
U Spec, 251
254 [t e rg => t e px & EXIST(c):[c e rf & t=g(c)]]
& [t e px & EXIST(c):[c e rf & t=g(c)] => t e rg]
Iff-And, 253
255 t e rg => t e px & EXIST(c):[c e rf & t=g(c)]
Split, 254
256 t e px & EXIST(c):[c e rf & t=g(c)] => t e rg
Split, 254
257 t e px & EXIST(c):[c e rf & t=g(c)]
Detach, 255, 252
258 t e px
Split, 257
259 EXIST(c):[c e rf & t=g(c)]
Split, 257
260 u e rf & t=g(u)
E Spec, 259
261 u e rf
Split, 260
262 t=g(u)
Split, 260
263 u e rf => ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
U Spec, 225
264 ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
Detach, 263, 261
265 u e rf <=> u e y & EXIST(c):[c e x & f(c)=u]
U Spec, 8
266 [u e rf => u e y & EXIST(c):[c e x & f(c)=u]]
& [u e y & EXIST(c):[c e x & f(c)=u] => u e rf]
Iff-And, 265
267 u e rf => u e y & EXIST(c):[c e x & f(c)=u]
Split, 266
268 u e y & EXIST(c):[c e x & f(c)=u] => u e rf
Split, 266
269 u e y & EXIST(c):[c e x & f(c)=u]
Detach, 267, 261
270 u e y
Split, 269
271 EXIST(c):[c e x & f(c)=u]
Split, 269
272 v e x & f(v)=u
E Spec, 271
273 v e x
Split, 272
274 f(v)=u
Split, 272
275 u e rf => ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
U Spec, 225
276 ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
Detach, 275, 261
277 v e x => [v e g(u) <=> f(v)=u]
U Spec, 276
278 v e g(u) <=> f(v)=u
Detach, 277, 273
279 [v e g(u) => f(v)=u] & [f(v)=u => v e g(u)]
Iff-And, 278
280 v e g(u) => f(v)=u
Split, 279
281 f(v)=u => v e g(u)
Split, 279
282 v e g(u)
Detach, 281, 274
283 v e t
Substitute, 262,
282
As Required:
284 ALL(a):[a e rg => EXIST(b):b e a]
4 Conclusion, 252
Construct the
choice function on the range of function g
Apply the Axiom of
Choice
285 ALL(f):[Set(f)
& ALL(a):[a e f => Set(a) & EXIST(b):b e a]
=>
EXIST(c):ALL(a):[a e f => c(a) e a]]
Choice
286 Set(rg) &
ALL(a):[a e rg => Set(a) & EXIST(b):b e a]
=>
EXIST(c):ALL(a):[a e rg => c(a) e a]
U Spec, 285
287 t e rg
Premise
288 t e rg <=> t e px & EXIST(c):[c e rf & t=g(c)]
U Spec, 251
289 [t e rg => t e px & EXIST(c):[c e rf & t=g(c)]]
& [t e px & EXIST(c):[c e rf & t=g(c)] => t e rg]
Iff-And, 288
290 t e rg => t e px & EXIST(c):[c e rf & t=g(c)]
Split, 289
291 t e px & EXIST(c):[c e rf & t=g(c)] => t e rg
Split, 289
292 t e px & EXIST(c):[c e rf & t=g(c)]
Detach, 290, 287
293 t e px
Split, 292
294 EXIST(c):[c e rf & t=g(c)]
Split, 292
295 t e px <=> Set(t) & ALL(d):[d e t => d e x]
U Spec, 14
296 [t e px => Set(t) & ALL(d):[d e t => d e x]]
& [Set(t) &
ALL(d):[d e t => d e x] => t e px]
Iff-And, 295
297 t e px => Set(t) & ALL(d):[d e t => d e x]
Split, 296
298 Set(t) &
ALL(d):[d e t => d e x] => t e px
Split, 296
299 Set(t) &
ALL(d):[d e t => d e x]
Detach, 297, 293
300 Set(t)
Split, 299
301 ALL(d):[d e t => d e x]
Split, 299
302 t e rg => EXIST(b):b e t
U Spec, 284
303 EXIST(b):b e t
Detach, 302, 287
304 Set(t) &
EXIST(b):b e t
Join, 300, 303
305 ALL(a):[a e rg => Set(a) & EXIST(b):b e a]
4 Conclusion, 287
306 Set(rg)
& ALL(a):[a e rg => Set(a) & EXIST(b):b e a]
Join, 250, 305
307 EXIST(c):ALL(a):[a e rg => c(a) e a]
Detach, 286, 306
Define: choice
(function)
308 ALL(a):[a e rg => choice(a) e a]
E Spec, 307
Construct the
required function h mapping the range of f back to the set x.
Apply the
Cartesian Product Axiom
309 ALL(a1):ALL(a2):[Set(a1)
& Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e a1 & c2 e a2]]]
Cart Prod
310 ALL(a2):[Set(rf) & Set(a2)
=> EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e a2]]]
U Spec, 309
311 Set(rf) & Set(x) =>
EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e x]]
U Spec, 310
312 Set(rf) & Set(x)
Join, 7, 2
313 EXIST(b):[Set'(b)
& ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e rf & c2 e x]]
Detach, 311, 312
314 Set'(rfx) &
ALL(c1):ALL(c2):[(c1,c2) e rfx <=> c1 e rf & c2 e x]
E Spec, 313
Define: rfx
315 Set'(rfx)
Split, 314
316 ALL(c1):ALL(c2):[(c1,c2) e rfx <=> c1 e rf & c2 e x]
Split, 314
317 EXIST(a):[Set'(a)
& ALL(b):ALL(c):[(b,c) e a <=>
(b,c) e rfx & c=choice(g(b))]]
Subset, 315
318 Set'(h) &
ALL(b):ALL(c):[(b,c) e h <=> (b,c) e rfx & c=choice(g(b))]
E Spec, 317
Define: h
319 Set'(h)
Split, 318
320 ALL(b):ALL(c):[(b,c) e h <=> (b,c) e rfx & c=choice(g(b))]
Split, 318
321 ALL(f):ALL(dom):ALL(cod):[Set'(f)
& Set(dom) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e f => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e f]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=> [(a1,b1) e f & (a1,b2) e f => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e dom & b e cod => [f(a1)=b <=> (a1,b) e f]]]]
Function
322 ALL(dom):ALL(cod):[Set'(h) & Set(dom)
& Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e h => a1 e dom & b e cod]
&
ALL(a1):[a1 e dom => EXIST(b):[b e cod & (a1,b) e h]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e dom & b1 e cod & b2 e cod
=> [(a1,b1) e h & (a1,b2) e h => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e dom & b e cod => [h(a1)=b <=> (a1,b) e h]]]]
U Spec, 321
323 ALL(cod):[Set'(h) & Set(rf) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e cod]
&
ALL(a1):[a1 e rf => EXIST(b):[b e cod & (a1,b) e h]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e cod & b2 e cod
=> [(a1,b1) e h & (a1,b2) e h => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e cod => [h(a1)=b <=>
(a1,b) e h]]]]
U Spec, 322
324 Set'(h) & Set(rf) & Set(x)
=>
[ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
&
ALL(a1):[a1 e rf => EXIST(b):[b e x & (a1,b) e h]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e x & b2 e x
=> [(a1,b1) e h & (a1,b2) e h => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e x => [h(a1)=b <=>
(a1,b) e h]]]
U Spec, 323
325 Set'(h) & Set(rf)
Join, 319, 7
326 Set'(h) & Set(rf) & Set(x)
Join, 325, 2
Sufficient: For
functionality of h
327 ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
&
ALL(a1):[a1 e rf => EXIST(b):[b e x & (a1,b) e h]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e x & b2 e x
=> [(a1,b1) e h & (a1,b2) e h => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e rf & b e x => [h(a1)=b <=>
(a1,b) e h]]
Detach, 324, 326
Prove:
ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
Suppose...
328 (t,u) e h
Premise
329 ALL(c):[(t,c) e h <=> (t,c) e rfx & c=choice(g(t))]
U Spec, 320
330 (t,u) e h <=> (t,u) e rfx & u=choice(g(t))
U Spec, 329
331 [(t,u) e h => (t,u) e rfx & u=choice(g(t))]
& [(t,u) e rfx & u=choice(g(t)) => (t,u) e h]
Iff-And, 330
332 (t,u) e h => (t,u) e rfx & u=choice(g(t))
Split, 331
333 (t,u) e rfx & u=choice(g(t)) => (t,u) e h
Split, 331
334 (t,u) e rfx & u=choice(g(t))
Detach, 332, 328
335 (t,u) e rfx
Split, 334
336 u=choice(g(t))
Split, 334
337 ALL(c2):[(t,c2) e rfx <=> t e rf & c2 e x]
U Spec, 316
338 (t,u) e rfx <=> t e rf & u e x
U Spec, 337
339 [(t,u) e rfx => t e rf & u e x]
& [t e rf & u e x => (t,u) e rfx]
Iff-And, 338
340 (t,u) e rfx => t e rf & u e x
Split, 339
341 t e rf & u e x => (t,u) e rfx
Split, 339
342 t e rf & u e x
Detach, 340, 335
As Required:
343 ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
4 Conclusion, 328
Prove:
ALL(a1):[a1 e rf => EXIST(b):[b e x &
(a1,b) e h]]
Suppose...
344 t e rf
Premise
345 t e rf => g(t) e px
U Spec, 201
346 g(t) e px
Detach, 345, 344
347 t e rf => ALL(d):[d e x => [d e g(t) <=> f(d)=t]]
U Spec, 225
348 ALL(d):[d e x => [d e g(t) <=> f(d)=t]]
Detach, 347, 344
349 g(t) e rg => choice(g(t)) e g(t)
U Spec, 308, 346
350 g(t) e rg <=> g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]
U Spec, 251, 346
351 [g(t) e rg => g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]]
& [g(t) e px & EXIST(c):[c e rf & g(t)=g(c)] => g(t) e rg]
Iff-And, 350
352 g(t) e rg => g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]
Split, 351
353 g(t) e px & EXIST(c):[c e rf & g(t)=g(c)] => g(t) e rg
Split, 351
354 g(t)=g(t)
Reflex, 346
355 t e rf & g(t)=g(t)
Join, 344, 354
356 EXIST(c):[c e rf & g(t)=g(c)]
E Gen, 355
357 g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]
Join, 346, 356
358 g(t) e rg
Detach, 353, 357
359 choice(g(t)) e g(t)
Detach, 349, 358
360 g(t) e px <=> Set(g(t)) & ALL(d):[d e g(t) => d e x]
U Spec, 14, 358
361 [g(t) e px => Set(g(t)) & ALL(d):[d e g(t) => d e x]]
& [Set(g(t)) &
ALL(d):[d e g(t) => d e x] => g(t) e px]
Iff-And, 360
362 g(t) e px => Set(g(t)) & ALL(d):[d e g(t) => d e x]
Split, 361
363 Set(g(t)) &
ALL(d):[d e g(t) => d e x] => g(t) e px
Split, 361
364 Set(g(t)) &
ALL(d):[d e g(t) => d e x]
Detach, 362, 346
365 Set(g(t))
Split, 364
366 ALL(d):[d e g(t) => d e x]
Split, 364
367 choice(g(t)) e g(t) => choice(g(t)) e x
U Spec, 366, 359
368 choice(g(t)) e x
Detach, 367, 359
369 ALL(c):[(t,c) e h <=> (t,c) e rfx & c=choice(g(t))]
U Spec, 320
370 (t,choice(g(t))) e h <=> (t,choice(g(t))) e rfx & choice(g(t))=choice(g(t))
U Spec, 369, 368
371 [(t,choice(g(t))) e h => (t,choice(g(t))) e rfx & choice(g(t))=choice(g(t))]
& [(t,choice(g(t))) e rfx & choice(g(t))=choice(g(t)) => (t,choice(g(t))) e h]
Iff-And, 370
372 (t,choice(g(t))) e h => (t,choice(g(t))) e rfx & choice(g(t))=choice(g(t))
Split, 371
373 (t,choice(g(t))) e rfx & choice(g(t))=choice(g(t)) => (t,choice(g(t))) e h
Split, 371
374 ALL(c2):[(t,c2) e rfx <=> t e rf & c2 e x]
U Spec, 316
375 (t,choice(g(t))) e rfx <=> t e rf & choice(g(t)) e x
U Spec, 374, 368
376 [(t,choice(g(t))) e rfx => t e rf & choice(g(t)) e x]
& [t e rf & choice(g(t)) e x => (t,choice(g(t))) e rfx]
Iff-And, 375
377 (t,choice(g(t))) e rfx => t e rf & choice(g(t)) e x
Split, 376
378 t e rf & choice(g(t)) e x => (t,choice(g(t))) e rfx
Split, 376
379 t e rf & choice(g(t)) e x
Join, 344, 368
380 (t,choice(g(t))) e rfx
Detach, 378, 379
381 choice(g(t))=choice(g(t))
Reflex, 368
382 (t,choice(g(t))) e rfx
& choice(g(t))=choice(g(t))
Join, 380, 381
383 (t,choice(g(t))) e h
Detach, 373, 382
384 choice(g(t)) e x & (t,choice(g(t))) e h
Join, 368, 383
385 EXIST(c):[c e x & (t,c) e h]
E Gen, 384
As Required:
386 ALL(a1):[a1 e rf => EXIST(c):[c e x & (a1,c) e h]]
4 Conclusion, 344
Prove:
ALL(a1):ALL(b1):ALL(b2):[a1 e rf & b1 e x & b2 e x
=> [(a1,b1) e h & (a1,b2) e h =>
b1=b2]]
Suppose...
387 t e rf & u1 e x & u2 e x
Premise
388 t e rf
Split, 387
389 u1 e x
Split, 387
390 u2 e x
Split, 387
Suppose...
391 (t,u1) e h & (t,u2) e h
Premise
392 (t,u1) e h
Split, 391
393 (t,u2) e h
Split, 391
394 ALL(c):[(t,c) e h <=> (t,c) e rfx & c=choice(g(t))]
U Spec, 320
395 (t,u1) e h <=> (t,u1) e rfx & u1=choice(g(t))
U Spec, 394
396 [(t,u1) e h => (t,u1) e rfx & u1=choice(g(t))]
&
[(t,u1) e rfx & u1=choice(g(t)) => (t,u1) e h]
Iff-And, 395
397 (t,u1) e h => (t,u1) e rfx & u1=choice(g(t))
Split, 396
398 (t,u1) e rfx & u1=choice(g(t)) => (t,u1) e h
Split, 396
399 (t,u1) e rfx & u1=choice(g(t))
Detach, 397, 392
400 (t,u1) e rfx
Split, 399
401 u1=choice(g(t))
Split, 399
402 (t,u2) e h <=> (t,u2) e rfx & u2=choice(g(t))
U Spec, 394
403 [(t,u2) e h => (t,u2) e rfx & u2=choice(g(t))]
&
[(t,u2) e rfx & u2=choice(g(t)) => (t,u2) e h]
Iff-And, 402
404 (t,u2) e h => (t,u2) e rfx & u2=choice(g(t))
Split, 403
405 (t,u2) e rfx & u2=choice(g(t)) => (t,u2) e h
Split, 403
406 (t,u2) e rfx & u2=choice(g(t))
Detach, 404, 393
407 (t,u2) e rfx
Split, 406
408 u2=choice(g(t))
Split, 406
409 u1=u2
Substitute, 408,
401
410 (t,u1) e h & (t,u2) e h => u1=u2
4 Conclusion, 391
As Required:
411 ALL(a):ALL(b1):ALL(b2):[a e rf & b1 e x & b2 e x
=> [(a,b1) e h & (a,b2) e h => b1=b2]]
4 Conclusion, 387
412 ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
&
ALL(a1):[a1 e rf => EXIST(c):[c e x & (a1,c) e h]]
Join, 343, 386
413 ALL(a1):ALL(b):[(a1,b) e h => a1 e rf & b e x]
&
ALL(a1):[a1 e rf => EXIST(c):[c e x & (a1,c) e h]]
&
ALL(a):ALL(b1):ALL(b2):[a e rf & b1 e x & b2 e x
=> [(a,b1) e h & (a,b2) e h => b1=b2]]
Join, 412, 411
h is a function
As Required:
414 ALL(a1):ALL(b):[a1 e rf & b e x => [h(a1)=b <=> (a1,b) e h]]
Detach, 327, 413
415 t e rf
Premise
416 t e rf => EXIST(c):[c e x & (t,c) e h]
U Spec, 386
417 EXIST(c):[c e x & (t,c) e h]
Detach, 416, 415
418 u e x & (t,u) e h
E Spec, 417
419 u e x
Split, 418
420 (t,u) e h
Split, 418
421 ALL(b):[t e rf & b e x => [h(t)=b <=> (t,b) e h]]
U Spec, 414
422 t e rf & u e x => [h(t)=u <=> (t,u) e h]
U Spec, 421
423 t e rf & u e x
Join, 415, 419
424 h(t)=u <=> (t,u) e h
Detach, 422, 423
425 [h(t)=u => (t,u) e h] & [(t,u) e h => h(t)=u]
Iff-And, 424
426 h(t)=u => (t,u) e h
Split, 425
427 (t,u) e h => h(t)=u
Split, 425
428 h(t)=u
Detach, 427, 420
429 h(t) e x
Substitute, 428,
419
Redefine: h
As Required:
430 ALL(a):[a e rf => h(a) e x]
4 Conclusion, 415
Suppose...
431 t e rf
Premise
432 t e rf => EXIST(c):[c e x & (t,c) e h]
U Spec, 386
433 EXIST(c):[c e x & (t,c) e h]
Detach, 432, 431
434 u e x & (t,u) e h
E Spec, 433
435 u e x
Split, 434
436 (t,u) e h
Split, 434
437 ALL(c):[(t,c) e h <=> (t,c) e rfx & c=choice(g(t))]
U Spec, 320
438 (t,u) e h <=> (t,u) e rfx & u=choice(g(t))
U Spec, 437
439 [(t,u) e h => (t,u) e rfx & u=choice(g(t))]
& [(t,u) e rfx & u=choice(g(t)) => (t,u) e h]
Iff-And, 438
440 (t,u) e h => (t,u) e rfx & u=choice(g(t))
Split, 439
441 (t,u) e rfx & u=choice(g(t)) => (t,u) e h
Split, 439
442 (t,u) e rfx & u=choice(g(t))
Detach, 440, 436
443 (t,u) e rfx
Split, 442
444 u=choice(g(t))
Split, 442
445 ALL(b):[t e rf & b e x => [h(t)=b <=> (t,b) e h]]
U Spec, 414
446 t e rf & u e x => [h(t)=u <=> (t,u) e h]
U Spec, 445
447 t e rf & u e x
Join, 431, 435
448 h(t)=u <=> (t,u) e h
Detach, 446, 447
449 [h(t)=u => (t,u) e h] & [(t,u) e h => h(t)=u]
Iff-And, 448
450 h(t)=u => (t,u) e h
Split, 449
451 (t,u) e h => h(t)=u
Split, 449
452 h(t)=u
Detach, 451, 436
453 h(t)=choice(g(t))
Substitute, 452,
444
As Required:
454 ALL(a):[a e rf => h(a)=choice(g(a))]
4 Conclusion, 431
Lemma
Prove:
ALL(a):ALL(b):ALL(c):[a e x & b e rf & c e rf => [a e g(b) & a e g(c) =>
b=c]]
Suppose...
455 p e x & t e rf & u e rf
Premise
456 p e x
Split, 455
457 t e rf
Split, 455
458 u e rf
Split, 455
Prove: p e g(t) & p e g(u) =>
t=u
Suppose...
459 p e g(t) & p e g(u)
Premise
460 p e g(t)
Split, 459
461 p e g(u)
Split, 459
462 t e rf => ALL(d):[d e x => [d e g(t) <=> f(d)=t]]
U Spec, 225
463 ALL(d):[d e x => [d e g(t) <=> f(d)=t]]
Detach, 462, 457
464 p e x => [p e g(t) <=> f(p)=t]
U Spec, 463
465 p e g(t) <=> f(p)=t
Detach, 464, 456
466 [p e g(t) => f(p)=t] & [f(p)=t => p e g(t)]
Iff-And, 465
467 p e g(t) => f(p)=t
Split, 466
468 f(p)=t => p e g(t)
Split, 466
469 f(p)=t
Detach, 467, 460
470 u e rf => ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
U Spec, 225
471 ALL(d):[d e x => [d e g(u) <=> f(d)=u]]
Detach, 470, 458
472 p e x => [p e g(u) <=> f(p)=u]
U Spec, 471
473 p e g(u) <=> f(p)=u
Detach, 472, 456
474 [p e g(u) => f(p)=u] & [f(p)=u => p e g(u)]
Iff-And, 473
475 p e g(u) => f(p)=u
Split, 474
476 f(p)=u => p e g(u)
Split, 474
477 f(p)=u
Detach, 475, 461
478 t=u
Substitute, 469,
477
As Required:
479 p e g(t) & p e g(u) => t=u
4 Conclusion, 459
Lemma
As Required:
480 ALL(a):ALL(b):ALL(c):[a e x & b e rf & c e rf => [a e g(b) & a e g(c) => b=c]]
4 Conclusion, 455
Prove: h is
injective
Suppose...
481 t e rf & u e rf
Premise
482 t e rf
Split, 481
483 u e rf
Split, 481
Prove:
h(t)=h(u) => t=u
Suppose...
484 h(t)=h(u)
Premise
485 t e rf => h(t)=choice(g(t))
U Spec, 454
486 h(t)=choice(g(t))
Detach, 485, 482
487 u e rf => h(u)=choice(g(u))
U Spec, 454
488 h(u)=choice(g(u))
Detach, 487, 483
489 choice(g(t))=h(u)
Substitute, 486,
484
490 choice(g(t))=choice(g(u))
Substitute, 488,
489
491 t e rf => g(t) e px
U Spec, 201
492 g(t) e px
Detach, 491, 482
493 g(t) e rg => choice(g(t)) e g(t)
U Spec, 308, 492
494 g(t) e rg <=> g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]
U Spec, 251, 492
495 [g(t) e rg => g(t) e px &
EXIST(c):[c e rf & g(t)=g(c)]]
& [g(t) e px & EXIST(c):[c e rf & g(t)=g(c)] => g(t) e rg]
Iff-And, 494
496 g(t) e rg => g(t) e px &
EXIST(c):[c e rf & g(t)=g(c)]
Split, 495
497 g(t) e px & EXIST(c):[c e rf & g(t)=g(c)] => g(t) e rg
Split, 495
498 g(t)=g(t)
Reflex, 492
499 t e rf & g(t)=g(t)
Join, 482, 498
500 EXIST(c):[c e rf & g(t)=g(c)]
E Gen, 499
501 g(t) e px & EXIST(c):[c e rf & g(t)=g(c)]
Join, 492, 500
502 g(t) e rg
Detach, 497, 501
503 choice(g(t)) e g(t)
Detach, 493, 502
504 u e rf => g(u) e px
U Spec, 201
505 g(u) e px
Detach, 504, 483
506 g(u) e rg => choice(g(u)) e g(u)
U Spec, 308, 505
507 g(u) e rg <=> g(u) e px & EXIST(c):[c e rf & g(u)=g(c)]
U Spec, 251, 505
508 [g(u) e rg => g(u) e px &
EXIST(c):[c e rf & g(u)=g(c)]]
& [g(u) e px & EXIST(c):[c e rf & g(u)=g(c)] => g(u) e rg]
Iff-And, 507
509 g(u) e rg => g(u) e px &
EXIST(c):[c e rf & g(u)=g(c)]
Split, 508
510 g(u) e px & EXIST(c):[c e rf & g(u)=g(c)] => g(u) e rg
Split, 508
511 g(u)=g(u)
Reflex, 505
512 u e rf & g(u)=g(u)
Join, 483, 511
513 EXIST(c):[c e rf & g(u)=g(c)]
E Gen, 512
514 g(u) e px & EXIST(c):[c e rf & g(u)=g(c)]
Join, 505, 513
515 g(u) e rg
Detach, 510, 514
516 choice(g(u)) e g(u)
Detach, 506, 515
517 choice(g(t)) e g(u)
Substitute, 490,
516
518 ALL(b):ALL(c):[choice(g(t)) e x & b e rf & c e rf => [choice(g(t)) e g(b) & choice(g(t)) e g(c) => b=c]]
U Spec, 480, 517
519 ALL(c):[choice(g(t)) e x & t e rf & c e rf => [choice(g(t)) e g(t) & choice(g(t)) e g(c) => t=c]]
U Spec, 518
520 choice(g(t)) e x & t e rf & u e rf => [choice(g(t)) e g(t) & choice(g(t)) e g(u) => t=u]
U Spec, 519
521 g(t) e px <=> Set(g(t)) &
ALL(d):[d e g(t) => d e x]
U Spec, 14, 502
522 [g(t) e px => Set(g(t)) &
ALL(d):[d e g(t) => d e x]]
&
[Set(g(t)) &
ALL(d):[d e g(t) => d e x] => g(t) e px]
Iff-And, 521
523 g(t) e px => Set(g(t)) &
ALL(d):[d e g(t) => d e x]
Split, 522
524 Set(g(t)) & ALL(d):[d e g(t) => d e x] => g(t) e px
Split, 522
525 Set(g(t)) & ALL(d):[d e g(t) => d e x]
Detach, 523, 492
526 Set(g(t))
Split, 525
527 ALL(d):[d e g(t) => d e x]
Split, 525
528 choice(g(t)) e g(t) => choice(g(t)) e x
U Spec, 527, 517
529 choice(g(t)) e x
Detach, 528, 503
530 choice(g(t)) e x & t e rf
Join, 529, 482
531 choice(g(t)) e x & t e rf & u e rf
Join, 530, 483
532 choice(g(t)) e g(t) & choice(g(t)) e g(u) => t=u
Detach, 520, 531
533 choice(g(t)) e g(t) & choice(g(t)) e g(u)
Join, 503, 517
534 t=u
Detach, 532, 533
As Required:
535 h(t)=h(u) => t=u
4 Conclusion, 484
h is injective
As Required:
536 ALL(a):ALL(b):[a e rf & b e rf => [h(a)=h(b) => a=b]]
4 Conclusion, 481
Getting rid of
rf term...
Prove:
ALL(a):[a e y & EXIST(b):[b e x &
f(b)=a] => h(a) e x]
Suppose...
537 t e y & EXIST(b):[b e x & f(b)=t]
Premise
538 t e rf => h(t) e x
U Spec, 430
539 t e rf <=> t e y & EXIST(c):[c e x & f(c)=t]
U Spec, 8
540 [t e rf => t e y & EXIST(c):[c e x & f(c)=t]]
& [t e y & EXIST(c):[c e x & f(c)=t] => t e rf]
Iff-And, 539
541 t e rf => t e y & EXIST(c):[c e x & f(c)=t]
Split, 540
542 t e y & EXIST(c):[c e x & f(c)=t] => t e rf
Split, 540
543 t e rf
Detach, 542, 537
544 h(t) e x
Detach, 538, 543
As Required:
545 ALL(a):[a e y & EXIST(b):[b e x & f(b)=a] => h(a) e x]
4 Conclusion, 537
Prove:
ALL(a):ALL(b):[a e y & b e y & EXIST(c):[c e x &
f(c)=a] & EXIST(d):[d e x &
f(d)=b]
=> [h(a)=h(b) => a=b]]
Suppose...
546 t e y & u e y &
EXIST(c):[c e x & f(c)=t] & EXIST(d):[d e x & f(d)=u]
Premise
547 t e y
Split, 546
548 u e y
Split, 546
549 EXIST(c):[c e x & f(c)=t]
Split, 546
550 EXIST(d):[d e x & f(d)=u]
Split, 546
551 ALL(b):[t e rf & b e rf => [h(t)=h(b) => t=b]]
U Spec, 536
Sufficient:
For h(t)=h(u) => t=u
552 t e rf & u e rf => [h(t)=h(u) => t=u]
U Spec, 551
553 t e rf <=> t e y & EXIST(c):[c e x & f(c)=t]
U Spec, 8
554 [t e rf => t e y & EXIST(c):[c e x & f(c)=t]]
& [t e y & EXIST(c):[c e x & f(c)=t] => t e rf]
Iff-And, 553
555 t e rf => t e y & EXIST(c):[c e x & f(c)=t]
Split, 554
556 t e y & EXIST(c):[c e x & f(c)=t] => t e rf
Split, 554
557 t e y & EXIST(c):[c e x & f(c)=t]
Join, 547, 549
558 t e rf
Detach, 556, 557
559 u e rf <=> u e y & EXIST(c):[c e x & f(c)=u]
U Spec, 8
560 [u e rf => u e y & EXIST(c):[c e x & f(c)=u]]
& [u e y & EXIST(c):[c e x & f(c)=u] => u e rf]
Iff-And, 559
561 u e rf => u e y & EXIST(c):[c e x & f(c)=u]
Split, 560
562 u e y & EXIST(c):[c e x & f(c)=u] => u e rf
Split, 560
563 u e y & EXIST(d):[d e x & f(d)=u]
Join, 548, 550
564 u e rf
Detach, 562, 563
565 t e rf & u e rf
Join, 558, 564
566 h(t)=h(u) => t=u
Detach, 552, 565
As Required:
567 ALL(a):ALL(b):[a e y & b e y & EXIST(c):[c e x & f(c)=a] &
EXIST(d):[d e x & f(d)=b]
=> [h(a)=h(b) => a=b]]
4 Conclusion, 546
568 ALL(a):[a e y & EXIST(b):[b e x & f(b)=a] => h(a) e x]
&
ALL(a):ALL(b):[a e y & b e y &
EXIST(c):[c e x & f(c)=a] & EXIST(d):[d e x & f(d)=b]
=> [h(a)=h(b) => a=b]]
Join, 545, 567
As Required:
569 ALL(f):[ALL(a):[a e x => f(a) e y]
=>
EXIST(h):[ALL(a):[a e y & EXIST(b):[b e x & f(b)=a] => h(a) e x]
&
ALL(a):ALL(b):[a e y & b e y &
EXIST(c):[c e x & f(c)=a] & EXIST(d):[d e x & f(d)=b]
=> [h(a)=h(b)
=> a=b]]]]
4 Conclusion, 4
As Required:
570 ALL(x):ALL(y):[Set(x) & Set(y)
=> ALL(f):[ALL(a):[a e x => f(a) e y]
=> EXIST(h):[ALL(a):[a e y & EXIST(b):[b e x & f(b)=a]
=> h(a) e x]
& ALL(a):ALL(b):[a e y & b e y & EXIST(c):[c e x & f(c)=a] & EXIST(d):[d e x & f(d)=b]
=> [h(a)=h(b) =>
a=b]]]]]
4 Conclusion, 1