THEOREM
*******
For every function f1 mapping set s1 to set s2, there exists a function f2 that maps subsets of s1 to its image under f1.
ALL(s1):ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(s1) & Set(s2) & Set(ps1) & Set(ps2)
& ALL(a):[a e s1 => f1(a) e s2]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(b):[b e f2(a) <=> EXIST(c):[c e a & f1(c)=b]]]]]
PROOF
*****
Suppose...
1 Set(x) & Set(y) & Set(px) & Set(py)
& ALL(a):[a e x => f(a) e y]
& ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
& ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
Premise
2 Set(x)
Split, 1
3 Set(y)
Split, 1
4 Set(px)
Split, 1
5 Set(py)
Split, 1
f maps elements of set x to elements of set y
6 ALL(a):[a e x => f(a) e y]
Split, 1
px is the power set of x
7 ALL(a):[a e px <=> Set(a) & ALL(b):[b e a => b e x]]
Split, 1
py is the power set of y
8 ALL(a):[a e py <=> Set(a) & ALL(b):[b e a => b e y]]
Split, 1
Apply Cartesian Product Axiom
9 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
10 ALL(a2):[Set(px) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e a2]]]
U Spec, 9
11 Set(px) & Set(py) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e py]]
U Spec, 10
12 Set(px) & Set(py)
Join, 4, 5
13 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e px & c2 e py]]
Detach, 11, 12
14 Set'(pxpy) & ALL(c1):ALL(c2):[(c1,c2) e pxpy <=> c1 e px & c2 e py]
E Spec, 13
Define: pxpy (the Cartesian product of px and py)
************
15 Set'(pxpy)
Split, 14
16 ALL(c1):ALL(c2):[(c1,c2) e pxpy <=> c1 e px & c2 e py]
Split, 14
17 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e a & f(d)=c]]]]
Subset, 15
18 Set'(img) & ALL(a):ALL(b):[(a,b) e img <=> (a,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e a & f(d)=c]]]
E Spec, 17
Define: img (a subset of pxpy)
***********
19 Set'(img)
Split, 18
20 ALL(a):ALL(b):[(a,b) e img <=> (a,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e a & f(d)=c]]]
Split, 18
Prove: img is a function
Apply Function Axiom
21 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
22 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e img => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e img]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
=> ALL(c):ALL(d):[d=img(c) <=> (c,d) e img]]
U Spec, 21
23 ALL(b):[ALL(c):ALL(d):[(c,d) e img => c e px & d e b]
& ALL(c):[c e px => EXIST(d):[d e b & (c,d) e img]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
=> ALL(c):ALL(d):[d=img(c) <=> (c,d) e img]]
U Spec, 22
Sufficient: For functionality of img
24 ALL(c):ALL(d):[(c,d) e img => c e px & d e py]
& ALL(c):[c e px => EXIST(d):[d e py & (c,d) e img]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
=> ALL(c):ALL(d):[d=img(c) <=> (c,d) e img]
U Spec, 23
Prove: ALL(c):ALL(d):[(c,d) e img => c e px & d e py]
Suppose...
25 (p,q) e img
Premise
Apply definition of img
26 ALL(b):[(p,b) e img <=> (p,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e p & f(d)=c]]]
U Spec, 20
27 (p,q) e img <=> (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 26
28 [(p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]]
& [(p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img]
Iff-And, 27
29 (p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Split, 28
30 (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img
Split, 28
31 (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Detach, 29, 25
32 (p,q) e pxpy
Split, 31
33 ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Split, 31
34 ALL(c2):[(p,c2) e pxpy <=> p e px & c2 e py]
U Spec, 16
Apply definition of pxpy
35 (p,q) e pxpy <=> p e px & q e py
U Spec, 34
36 [(p,q) e pxpy => p e px & q e py]
& [p e px & q e py => (p,q) e pxpy]
Iff-And, 35
37 (p,q) e pxpy => p e px & q e py
Split, 36
38 p e px & q e py => (p,q) e pxpy
Split, 36
39 p e px & q e py
Detach, 37, 32
As Required:
40 ALL(c):ALL(d):[(c,d) e img => c e px & d e py]
4 Conclusion, 25
Prove: ALL(c):[c e px => EXIST(d):[d e py & (c,d) e img]]
Suppose...
41 p e px
Premise
Apply Subset Axiom
42 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e y & EXIST(b):[b e p & f(b)=a]]]
Subset, 3
43 Set(q) & ALL(a):[a e q <=> a e y & EXIST(b):[b e p & f(b)=a]]
E Spec, 42
44 Set(q)
Split, 43
q is the image of p under f
45 ALL(a):[a e q <=> a e y & EXIST(b):[b e p & f(b)=a]]
Split, 43
Apply the definition of img
46 ALL(b):[(p,b) e img <=> (p,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e p & f(d)=c]]]
U Spec, 20
47 (p,q) e img <=> (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 46
48 [(p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]]
& [(p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img]
Iff-And, 47
49 (p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Split, 48
50 (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img
Split, 48
51 ALL(c2):[(p,c2) e pxpy <=> p e px & c2 e py]
U Spec, 16
Apply the definition of pxpy
52 (p,q) e pxpy <=> p e px & q e py
U Spec, 51
53 [(p,q) e pxpy => p e px & q e py]
& [p e px & q e py => (p,q) e pxpy]
Iff-And, 52
54 (p,q) e pxpy => p e px & q e py
Split, 53
55 p e px & q e py => (p,q) e pxpy
Split, 53
Apply the definition of py
56 q e py <=> Set(q) & ALL(b):[b e q => b e y]
U Spec, 8
57 [q e py => Set(q) & ALL(b):[b e q => b e y]]
& [Set(q) & ALL(b):[b e q => b e y] => q e py]
Iff-And, 56
58 q e py => Set(q) & ALL(b):[b e q => b e y]
Split, 57
59 Set(q) & ALL(b):[b e q => b e y] => q e py
Split, 57
Prove: ALL(b):[b e q => b e y]
Suppose...
60 r e q
Premise
Apply definition of q
61 r e q <=> r e y & EXIST(b):[b e p & f(b)=r]
U Spec, 45
62 [r e q => r e y & EXIST(b):[b e p & f(b)=r]]
& [r e y & EXIST(b):[b e p & f(b)=r] => r e q]
Iff-And, 61
63 r e q => r e y & EXIST(b):[b e p & f(b)=r]
Split, 62
64 r e y & EXIST(b):[b e p & f(b)=r] => r e q
Split, 62
65 r e y & EXIST(b):[b e p & f(b)=r]
Detach, 63, 60
66 r e y
Split, 65
As Required:
67 ALL(b):[b e q => b e y]
4 Conclusion, 60
68 Set(q) & ALL(b):[b e q => b e y]
Join, 44, 67
69 q e py
Detach, 59, 68
70 p e px & q e py
Join, 41, 69
71 (p,q) e pxpy
Detach, 55, 70
Prove: ALL(c):[c e q => EXIST(b):[b e p & f(b)=c]]
Suppose...
72 r e q
Premise
Apply definition of q
73 r e q <=> r e y & EXIST(b):[b e p & f(b)=r]
U Spec, 45
74 [r e q => r e y & EXIST(b):[b e p & f(b)=r]]
& [r e y & EXIST(b):[b e p & f(b)=r] => r e q]
Iff-And, 73
75 r e q => r e y & EXIST(b):[b e p & f(b)=r]
Split, 74
76 r e y & EXIST(b):[b e p & f(b)=r] => r e q
Split, 74
77 r e y & EXIST(b):[b e p & f(b)=r]
Detach, 75, 72
78 r e y
Split, 77
79 EXIST(b):[b e p & f(b)=r]
Split, 77
As Required:
80 ALL(c):[c e q => EXIST(b):[b e p & f(b)=c]]
4 Conclusion, 72
Prove: ALL(c):[EXIST(b):[b e p & f(b)=c] => c e q]
Suppose...
81 EXIST(b):[b e p & f(b)=r]
Premise
Apply definition of q
82 r e q <=> r e y & EXIST(b):[b e p & f(b)=r]
U Spec, 45
83 [r e q => r e y & EXIST(b):[b e p & f(b)=r]]
& [r e y & EXIST(b):[b e p & f(b)=r] => r e q]
Iff-And, 82
84 r e q => r e y & EXIST(b):[b e p & f(b)=r]
Split, 83
85 r e y & EXIST(b):[b e p & f(b)=r] => r e q
Split, 83
86 s e p & f(s)=r
E Spec, 81
87 s e p
Split, 86
88 f(s)=r
Split, 86
Apply definition of px
89 p e px <=> Set(p) & ALL(b):[b e p => b e x]
U Spec, 7
90 [p e px => Set(p) & ALL(b):[b e p => b e x]]
& [Set(p) & ALL(b):[b e p => b e x] => p e px]
Iff-And, 89
91 p e px => Set(p) & ALL(b):[b e p => b e x]
Split, 90
92 Set(p) & ALL(b):[b e p => b e x] => p e px
Split, 90
93 Set(p) & ALL(b):[b e p => b e x]
Detach, 91, 41
94 Set(p)
Split, 93
95 ALL(b):[b e p => b e x]
Split, 93
96 s e p => s e x
U Spec, 95
97 s e x
Detach, 96, 87
98 s e x => f(s) e y
U Spec, 6
99 f(s) e y
Detach, 98, 97
100 r e y
Substitute, 88, 99
101 r e y & EXIST(b):[b e p & f(b)=r]
Join, 100, 81
102 r e q
Detach, 85, 101
As Required:
103 ALL(c):[EXIST(b):[b e p & f(b)=c] => c e q]
4 Conclusion, 81
104 ALL(c):[[c e q => EXIST(b):[b e p & f(b)=c]] & [EXIST(b):[b e p & f(b)=c] => c e q]]
Join, 80, 103
105 ALL(c):[c e q <=> EXIST(b):[b e p & f(b)=c]]
Iff-And, 104
106 (p,q) e pxpy
& ALL(c):[c e q <=> EXIST(b):[b e p & f(b)=c]]
Join, 71, 105
107 (p,q) e img
Detach, 50, 106
108 q e py & (p,q) e img
Join, 69, 107
As Required:
109 ALL(c):[c e px => EXIST(d):[d e py & (c,d) e img]]
4 Conclusion, 41
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
Suppose...
110 (p,q1) e img & (p,q2) e img
Premise
111 (p,q1) e img
Split, 110
112 (p,q2) e img
Split, 110
Apply Set Equality Axiom
113 ALL(a):ALL(b):[Set(a) & Set(b) => [a=b <=> ALL(c):[c e a <=> c e b]]]
Set Equality
114 ALL(b):[Set(q1) & Set(b) => [q1=b <=> ALL(c):[c e q1 <=> c e b]]]
U Spec, 113
115 Set(q1) & Set(q2) => [q1=q2 <=> ALL(c):[c e q1 <=> c e q2]]
U Spec, 114
Apply definiton of img
116 ALL(b):[(p,b) e img <=> (p,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e p & f(d)=c]]]
U Spec, 20
117 (p,q1) e img <=> (p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 116
118 [(p,q1) e img => (p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]]]
& [(p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]] => (p,q1) e img]
Iff-And, 117
119 (p,q1) e img => (p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]]
Split, 118
120 (p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]] => (p,q1) e img
Split, 118
121 (p,q1) e pxpy & ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]]
Detach, 119, 111
122 (p,q1) e pxpy
Split, 121
123 ALL(c):[c e q1 <=> EXIST(d):[d e p & f(d)=c]]
Split, 121
Apply definition of pxpy
124 ALL(c2):[(p,c2) e pxpy <=> p e px & c2 e py]
U Spec, 16
125 (p,q1) e pxpy <=> p e px & q1 e py
U Spec, 124
126 [(p,q1) e pxpy => p e px & q1 e py]
& [p e px & q1 e py => (p,q1) e pxpy]
Iff-And, 125
127 (p,q1) e pxpy => p e px & q1 e py
Split, 126
128 p e px & q1 e py => (p,q1) e pxpy
Split, 126
129 p e px & q1 e py
Detach, 127, 122
130 p e px
Split, 129
131 q1 e py
Split, 129
Apply definition of py
132 q1 e py <=> Set(q1) & ALL(b):[b e q1 => b e y]
U Spec, 8
133 [q1 e py => Set(q1) & ALL(b):[b e q1 => b e y]]
& [Set(q1) & ALL(b):[b e q1 => b e y] => q1 e py]
Iff-And, 132
134 q1 e py => Set(q1) & ALL(b):[b e q1 => b e y]
Split, 133
135 Set(q1) & ALL(b):[b e q1 => b e y] => q1 e py
Split, 133
136 Set(q1) & ALL(b):[b e q1 => b e y]
Detach, 134, 131
137 Set(q1)
Split, 136
138 ALL(b):[b e q1 => b e y]
Split, 136
Apply definition of img
139 (p,q2) e img <=> (p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 116
140 [(p,q2) e img => (p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]]]
& [(p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]] => (p,q2) e img]
Iff-And, 139
141 (p,q2) e img => (p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]]
Split, 140
142 (p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]] => (p,q2) e img
Split, 140
143 (p,q2) e pxpy & ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]]
Detach, 141, 112
144 (p,q2) e pxpy
Split, 143
145 ALL(c):[c e q2 <=> EXIST(d):[d e p & f(d)=c]]
Split, 143
Apply definition of pxpy
146 (p,q2) e pxpy <=> p e px & q2 e py
U Spec, 124
147 [(p,q2) e pxpy => p e px & q2 e py]
& [p e px & q2 e py => (p,q2) e pxpy]
Iff-And, 146
148 (p,q2) e pxpy => p e px & q2 e py
Split, 147
149 p e px & q2 e py => (p,q2) e pxpy
Split, 147
150 p e px & q2 e py
Detach, 148, 144
151 p e px
Split, 150
152 q2 e py
Split, 150
Apply definition of py
153 q2 e py <=> Set(q2) & ALL(b):[b e q2 => b e y]
U Spec, 8
154 [q2 e py => Set(q2) & ALL(b):[b e q2 => b e y]]
& [Set(q2) & ALL(b):[b e q2 => b e y] => q2 e py]
Iff-And, 153
155 q2 e py => Set(q2) & ALL(b):[b e q2 => b e y]
Split, 154
156 Set(q2) & ALL(b):[b e q2 => b e y] => q2 e py
Split, 154
157 Set(q2) & ALL(b):[b e q2 => b e y]
Detach, 155, 152
158 Set(q2)
Split, 157
159 ALL(b):[b e q2 => b e y]
Split, 157
160 Set(q1) & Set(q2)
Join, 137, 158
161 q1=q2 <=> ALL(c):[c e q1 <=> c e q2]
Detach, 115, 160
162 [q1=q2 => ALL(c):[c e q1 <=> c e q2]]
& [ALL(c):[c e q1 <=> c e q2] => q1=q2]
Iff-And, 161
163 q1=q2 => ALL(c):[c e q1 <=> c e q2]
Split, 162
Sufficient:
164 ALL(c):[c e q1 <=> c e q2] => q1=q2
Split, 162
Prove: ALL(c):[c e q1 => c e q2]
Suppose...
165 r e q1
Premise
Apply definition of q1
166 r e q1 <=> EXIST(d):[d e p & f(d)=r]
U Spec, 123
167 [r e q1 => EXIST(d):[d e p & f(d)=r]]
& [EXIST(d):[d e p & f(d)=r] => r e q1]
Iff-And, 166
168 r e q1 => EXIST(d):[d e p & f(d)=r]
Split, 167
169 EXIST(d):[d e p & f(d)=r] => r e q1
Split, 167
170 EXIST(d):[d e p & f(d)=r]
Detach, 168, 165
171 s e p & f(s)=r
E Spec, 170
172 s e p
Split, 171
173 f(s)=r
Split, 171
Apply definition of q2
174 r e q2 <=> EXIST(d):[d e p & f(d)=r]
U Spec, 145
175 [r e q2 => EXIST(d):[d e p & f(d)=r]]
& [EXIST(d):[d e p & f(d)=r] => r e q2]
Iff-And, 174
176 r e q2 => EXIST(d):[d e p & f(d)=r]
Split, 175
177 EXIST(d):[d e p & f(d)=r] => r e q2
Split, 175
178 s e p & f(s)=r
Join, 172, 173
179 EXIST(d):[d e p & f(d)=r]
E Gen, 178
180 r e q2
Detach, 177, 179
As Required:
181 ALL(c):[c e q1 => c e q2]
4 Conclusion, 165
Prove: ALL(c):[c e q2 => c e q1]
Suppose...
182 r e q2
Premise
Apply definition of q2
183 r e q2 <=> EXIST(d):[d e p & f(d)=r]
U Spec, 145
184 [r e q2 => EXIST(d):[d e p & f(d)=r]]
& [EXIST(d):[d e p & f(d)=r] => r e q2]
Iff-And, 183
185 r e q2 => EXIST(d):[d e p & f(d)=r]
Split, 184
186 EXIST(d):[d e p & f(d)=r] => r e q2
Split, 184
187 EXIST(d):[d e p & f(d)=r]
Detach, 185, 182
Apply definition of q1
188 r e q1 <=> EXIST(d):[d e p & f(d)=r]
U Spec, 123
189 [r e q1 => EXIST(d):[d e p & f(d)=r]]
& [EXIST(d):[d e p & f(d)=r] => r e q1]
Iff-And, 188
190 r e q1 => EXIST(d):[d e p & f(d)=r]
Split, 189
191 EXIST(d):[d e p & f(d)=r] => r e q1
Split, 189
192 r e q1
Detach, 191, 187
As Required:
193 ALL(c):[c e q2 => c e q1]
4 Conclusion, 182
194 ALL(c):[[c e q1 => c e q2] & [c e q2 => c e q1]]
Join, 181, 193
195 ALL(c):[c e q1 <=> c e q2]
Iff-And, 194
196 q1=q2
Detach, 164, 195
As Required:
197 ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
4 Conclusion, 110
198 ALL(c):ALL(d):[(c,d) e img => c e px & d e py]
& ALL(c):[c e px => EXIST(d):[d e py & (c,d) e img]]
Join, 40, 109
199 ALL(c):ALL(d):[(c,d) e img => c e px & d e py]
& ALL(c):[c e px => EXIST(d):[d e py & (c,d) e img]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e img & (c,d2) e img => d1=d2]
Join, 198, 197
As Required: img is a function
200 ALL(c):ALL(d):[d=img(c) <=> (c,d) e img]
Detach, 24, 199
Prove: ALL(a):[a e px => img(a) e py]
Suppose...
201 p e px
Premise
Apply definition of px
202 p e px => EXIST(d):[d e py & (p,d) e img]
U Spec, 109
203 EXIST(d):[d e py & (p,d) e img]
Detach, 202, 201
204 q e py & (p,q) e img
E Spec, 203
205 q e py
Split, 204
206 (p,q) e img
Split, 204
Apply functionality of img
207 ALL(d):[d=img(p) <=> (p,d) e img]
U Spec, 200
208 q=img(p) <=> (p,q) e img
U Spec, 207
209 [q=img(p) => (p,q) e img] & [(p,q) e img => q=img(p)]
Iff-And, 208
210 q=img(p) => (p,q) e img
Split, 209
211 (p,q) e img => q=img(p)
Split, 209
212 q=img(p)
Detach, 211, 206
213 img(p) e py
Substitute, 212, 205
As Required:
214 ALL(a):[a e px => img(a) e py]
4 Conclusion, 201
Prove: ALL(a):[a e px => ALL(c):[c e img(a) <=> EXIST(d):[d e a & f(d)=c]]]
Suppose...
215 p e px
Premise
216 p e px => EXIST(d):[d e py & (p,d) e img]
U Spec, 109
217 EXIST(d):[d e py & (p,d) e img]
Detach, 216, 215
218 q e py & (p,q) e img
E Spec, 217
219 q e py
Split, 218
220 (p,q) e img
Split, 218
Apply definition of img
221 ALL(b):[(p,b) e img <=> (p,b) e pxpy & ALL(c):[c e b <=> EXIST(d):[d e p & f(d)=c]]]
U Spec, 20
222 (p,q) e img <=> (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
U Spec, 221
223 [(p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]]
& [(p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img]
Iff-And, 222
224 (p,q) e img => (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Split, 223
225 (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]] => (p,q) e img
Split, 223
226 (p,q) e pxpy & ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Detach, 224, 220
227 (p,q) e pxpy
Split, 226
228 ALL(c):[c e q <=> EXIST(d):[d e p & f(d)=c]]
Split, 226
Apply functionality of img
229 ALL(d):[d=img(p) <=> (p,d) e img]
U Spec, 200
230 q=img(p) <=> (p,q) e img
U Spec, 229
231 [q=img(p) => (p,q) e img] & [(p,q) e img => q=img(p)]
Iff-And, 230
232 q=img(p) => (p,q) e img
Split, 231
233 (p,q) e img => q=img(p)
Split, 231
234 q=img(p)
Detach, 233, 220
235 ALL(c):[c e img(p) <=> EXIST(d):[d e p & f(d)=c]]
Substitute, 234, 228
As Required:
236 ALL(a):[a e px
=> ALL(c):[c e img(a) <=> EXIST(d):[d e a & f(d)=c]]]
4 Conclusion, 215
237 ALL(a):[a e px => img(a) e py]
& ALL(a):[a e px
=> ALL(c):[c e img(a) <=> EXIST(d):[d e a & f(d)=c]]]
Join, 214, 236
As Required:
238 ALL(s1):ALL(s2):ALL(ps1):ALL(ps2):ALL(f1):[Set(s1) & Set(s2) & Set(ps1) & Set(ps2)
& ALL(a):[a e s1 => f1(a) e s2]
& ALL(a):[a e ps1 <=> Set(a) & ALL(b):[b e a => b e s1]]
& ALL(a):[a e ps2 <=> Set(a) & ALL(b):[b e a => b e s2]]
=> EXIST(f2):[ALL(a):[a e ps1 => f2(a) e ps2]
& ALL(a):[a e ps1
=> ALL(c):[c e f2(a) <=> EXIST(d):[d e a & f1(d)=c]]]]]
4 Conclusion, 1