THEOREM
-------
ALL(a):[Subset(a,sA) => a=pre(img(a))] <=> FOnto
where
f is a function mapping set sA to set sB
img(x) = the image set of set x under f
pre(x) = the pre-image set of x under f
Subset(x,y) means x is a subset of y
FOnto means f is injective (onto)
& means AND
| means OR
=> means IMPLIES
<=> means IF AND ONLY IF
By Dan Christensen
This proof written using proof assistant software developed by the author and available free at:
OUTLINE
-------
Let f be a function mapping set sA to set sB.
Suppose f is onto.
Suppose s is a subset of sA. Prove s = pre(img(s))
'=>'
Suppose x e s
Show x e pre(img(s)
'<='
Suppose ~ x e s (proof by contrapositive)
Case 1: Suppose x e sA
Suppose x e pre(img(s))
Obtain contradiction.
Case 2: Suppose ~ x e sA
Show ~ x e pre(img(s))
Therefore, s = pre(img(s))
Suppose f is not onto. (proof by contrapositive)
Let x and y be distinct elements of sA such that f(x)=f(y).
Construct the singleton {x} (a subset of sA).
Show {x} not equal to pre(img({x})).
Therefore, not all subsets s of sA are such that s = pre(img(s)).
AXIOMS/DEFINITIONS
------------------
Define: set equality
1 ALL(a):ALL(b):[a=b <=> ALL(c):[c e a <=> c e b]]
Axiom
Define: Subset
2 ALL(a):ALL(b):[Subset(a,b) <=> ALL(c):[c e a => c e b]]
Axiom
Define: Sets sA and sB
3 Set(sA)
Axiom
4 Set(sB)
Axiom
Define: f
f is a function mapping set sA to set sB
5 ALL(a):[a e sA => f(a) e sB]
Axiom
Define: FOnto (f is injective (onto))
6 FOnto <=> ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Axiom
Define: img
img(x) = the image set of set x under f
7 ALL(a):[Subset(a,sA) => Subset(img(a),sB)
& ALL(b):[b e img(a) <=> EXIST(c):[c e a & f(c)=b]]]
Axiom
Define: pre
pre(x) = the pre-image set of set x under f
8 ALL(a):[Subset(a,sB) => Subset(pre(a),sA)
& ALL(b):[b e pre(a) <=> EXIST(c):[c e a & f(b)=c]]]
Axiom
Prove: FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]
Suppose...
9 FOnto
Premise
Apply definition of FOnto
10 [FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]]
& [ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto]
Iff-And, 6
11 FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Split, 10
12 ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto
Split, 10
13 ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Detach, 11, 9
Prove: ALL(a):[Subset(a,sA) => a=pre(img(a))]
Suppose...
14 Subset(s,sA)
Premise
Apply definiton of Subset
15 ALL(b):[Subset(s,b) <=> ALL(c):[c e s => c e b]]
U Spec, 2
16 Subset(s,sA) <=> ALL(c):[c e s => c e sA]
U Spec, 15
17 [Subset(s,sA) => ALL(c):[c e s => c e sA]]
& [ALL(c):[c e s => c e sA] => Subset(s,sA)]
Iff-And, 16
18 Subset(s,sA) => ALL(c):[c e s => c e sA]
Split, 17
19 ALL(c):[c e s => c e sA] => Subset(s,sA)
Split, 17
20 ALL(c):[c e s => c e sA]
Detach, 18, 14
Apply definition of img
21 Subset(s,sA) => Subset(img(s),sB)
& ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]
U Spec, 7
22 Subset(img(s),sB)
& ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]
Detach, 21, 14
23 Subset(img(s),sB)
Split, 22
24 ALL(b):[b e img(s) <=> EXIST(c):[c e s & f(c)=b]]
Split, 22
Apply definiton of pre
25 Subset(img(s),sB) => Subset(pre(img(s)),sA)
& ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]
U Spec, 8
26 Subset(pre(img(s)),sA)
& ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]
Detach, 25, 23
27 Subset(pre(img(s)),sA)
Split, 26
28 ALL(b):[b e pre(img(s)) <=> EXIST(c):[c e img(s) & f(b)=c]]
Split, 26
29 ALL(b):[s=b <=> ALL(c):[c e s <=> c e b]]
U Spec, 1
30 s=pre(img(s)) <=> ALL(c):[c e s <=> c e pre(img(s))]
U Spec, 29
31 [s=pre(img(s)) => ALL(c):[c e s <=> c e pre(img(s))]]
& [ALL(c):[c e s <=> c e pre(img(s))] => s=pre(img(s))]
Iff-And, 30
32 s=pre(img(s)) => ALL(c):[c e s <=> c e pre(img(s))]
Split, 31
Sufficient: For s=pre(img(s))
33 ALL(c):[c e s <=> c e pre(img(s))] => s=pre(img(s))
Split, 31
Prove: ALL(c):[c e s => c e pre(img(s))]
Suppose...
34 x e s
Premise
Apply definition of pre
35 x e pre(img(s)) <=> EXIST(c):[c e img(s) & f(x)=c]
U Spec, 28
36 [x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]]
& [EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))]
Iff-And, 35
37 x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]
Split, 36
Sufficient: For x e pre(img(s))
38 EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))
Split, 36
Apply definition of img
39 f(x) e img(s) <=> EXIST(c):[c e s & f(c)=f(x)]
U Spec, 24
40 [f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]]
& [EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)]
Iff-And, 39
41 f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]
Split, 40
Sufficient: For f(x) e img(s)
42 EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)
Split, 40
43 f(x)=f(x)
Reflex
44 x e s & f(x)=f(x)
Join, 34, 43
45 EXIST(c):[c e s & f(c)=f(x)]
E Gen, 44
46 f(x) e img(s)
Detach, 42, 45
47 f(x) e img(s) & f(x)=f(x)
Join, 46, 43
48 EXIST(c):[c e img(s) & f(x)=c]
E Gen, 47
49 x e pre(img(s))
Detach, 38, 48
As Required:
50 ALL(c):[c e s => c e pre(img(s))]
4 Conclusion, 34
Prove: ALL(c):[~c e s => ~c e pre(img(s))]
Suppose...
51 ~x e s
Premise
Two cases to consider:
52 x e sA | ~x e sA
Or Not
Case 1:
Prove: x e sA => ~x e pre(img(s))
Suppose...
53 x e sA
Premise
Suppose to the contrary...
54 x e pre(img(s))
Premise
Apply definition of pre
55 x e pre(img(s)) <=> EXIST(c):[c e img(s) & f(x)=c]
U Spec, 28
56 [x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]]
& [EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))]
Iff-And, 55
57 x e pre(img(s)) => EXIST(c):[c e img(s) & f(x)=c]
Split, 56
58 EXIST(c):[c e img(s) & f(x)=c] => x e pre(img(s))
Split, 56
59 EXIST(c):[c e img(s) & f(x)=c]
Detach, 57, 54
60 y e img(s) & f(x)=y
E Spec, 59
Define: y
61 y e img(s)
Split, 60
62 f(x)=y
Split, 60
63 f(x) e img(s)
Substitute, 62, 61
Apply definition of img
64 f(x) e img(s) <=> EXIST(c):[c e s & f(c)=f(x)]
U Spec, 24
65 [f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]]
& [EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)]
Iff-And, 64
66 f(x) e img(s) => EXIST(c):[c e s & f(c)=f(x)]
Split, 65
67 EXIST(c):[c e s & f(c)=f(x)] => f(x) e img(s)
Split, 65
68 EXIST(c):[c e s & f(c)=f(x)]
Detach, 66, 63
69 z e s & f(z)=f(x)
E Spec, 68
70 z e s
Split, 69
71 f(z)=f(x)
Split, 69
Apply definition of FOnto
72 ALL(b):[z e sA & b e sA => [f(z)=f(b) => z=b]]
U Spec, 13
73 z e sA & x e sA => [f(z)=f(x) => z=x]
U Spec, 72
74 z e s => z e sA
U Spec, 20
75 z e sA
Detach, 74, 70
76 z e sA & x e sA
Join, 75, 53
77 f(z)=f(x) => z=x
Detach, 73, 76
78 z=x
Detach, 77, 71
79 x e s
Substitute, 78, 70
80 x e s & ~x e s
Join, 79, 51
As Required:
81 ~x e pre(img(s))
4 Conclusion, 54
As Required:
82 x e sA => ~x e pre(img(s))
4 Conclusion, 53
Case 2:
Prove: ~x e sA => ~x e pre(img(s))
Suppose...
83 ~x e sA
Premise
Apply definition of Subset
84 ALL(b):[Subset(pre(img(s)),b) <=> ALL(c):[c e pre(img(s)) => c e b]]
U Spec, 2
85 Subset(pre(img(s)),sA) <=> ALL(c):[c e pre(img(s)) => c e sA]
U Spec, 84
86 [Subset(pre(img(s)),sA) => ALL(c):[c e pre(img(s)) => c e sA]]
& [ALL(c):[c e pre(img(s)) => c e sA] => Subset(pre(img(s)),sA)]
Iff-And, 85
87 Subset(pre(img(s)),sA) => ALL(c):[c e pre(img(s)) => c e sA]
Split, 86
88 ALL(c):[c e pre(img(s)) => c e sA] => Subset(pre(img(s)),sA)
Split, 86
89 ALL(c):[c e pre(img(s)) => c e sA]
Detach, 87, 27
90 x e pre(img(s)) => x e sA
U Spec, 89
91 ~x e sA => ~x e pre(img(s))
Contra, 90
92 ~x e pre(img(s))
Detach, 91, 83
As Required:
93 ~x e sA => ~x e pre(img(s))
4 Conclusion, 83
94 [x e sA => ~x e pre(img(s))]
& [~x e sA => ~x e pre(img(s))]
Join, 82, 93
95 ~x e pre(img(s))
Cases, 52, 94
As Required:
96 ALL(c):[~c e s => ~c e pre(img(s))]
4 Conclusion, 51
97 ALL(c):[~~c e pre(img(s)) => ~~c e s]
Contra, 96
98 ALL(c):[c e pre(img(s)) => ~~c e s]
Rem DNeg, 97
99 ALL(c):[c e pre(img(s)) => c e s]
Rem DNeg, 98
100 ALL(c):[[c e s => c e pre(img(s))] & [c e pre(img(s)) => c e s]]
Join, 50, 99
101 ALL(c):[c e s <=> c e pre(img(s))]
Iff-And, 100
102 s=pre(img(s))
Detach, 33, 101
As Required:
103 ALL(a):[Subset(a,sA) => a=pre(img(a))]
4 Conclusion, 14
As Required:
104 FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]
4 Conclusion, 9
Prove: ~FOnto => ~ALL(a):[Subset(a,sA) => a=pre(img(a))]
Suppose...
105 ~FOnto
Premise
Apply definition of FOnto
106 [FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]]
& [ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto]
Iff-And, 6
107 FOnto => ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Split, 106
108 ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]] => FOnto
Split, 106
109 ~FOnto => ~ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Contra, 108
110 ~ALL(a):ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Detach, 109, 105
111 ~~EXIST(a):~ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Quant, 110
112 EXIST(a):~ALL(b):[a e sA & b e sA => [f(a)=f(b) => a=b]]
Rem DNeg, 111
113 EXIST(a):~~EXIST(b):~[a e sA & b e sA => [f(a)=f(b) => a=b]]
Quant, 112
114 EXIST(a):EXIST(b):~[a e sA & b e sA => [f(a)=f(b) => a=b]]
Rem DNeg, 113
115 EXIST(a):EXIST(b):~~[a e sA & b e sA & ~[f(a)=f(b) => a=b]]
Imply-And, 114
116 EXIST(a):EXIST(b):[a e sA & b e sA & ~[f(a)=f(b) => a=b]]
Rem DNeg, 115
117 EXIST(a):EXIST(b):[a e sA & b e sA & ~~[f(a)=f(b) & ~a=b]]
Imply-And, 116
118 EXIST(a):EXIST(b):[a e sA & b e sA & [f(a)=f(b) & ~a=b]]
Rem DNeg, 117
119 EXIST(b):[x e sA & b e sA & [f(x)=f(b) & ~x=b]]
E Spec, 118
120 x e sA & y e sA & [f(x)=f(y) & ~x=y]
E Spec, 119
Define: x and y (distinct elements of sA with identical images under f)
121 x e sA
Split, 120
122 y e sA
Split, 120
123 f(x)=f(y) & ~x=y
Split, 120
124 f(x)=f(y)
Split, 123
125 ~x=y
Split, 123
Construct the singleton {x}
Apply the Subset Axiom
126 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e sA & a=x]]
Subset, 3
127 Set(onlyX) & ALL(a):[a e onlyX <=> a e sA & a=x]
E Spec, 126
Define: onlyX (subset of sA, a singleton)
128 Set(onlyX)
Split, 127
129 ALL(a):[a e onlyX <=> a e sA & a=x]
Split, 127
Apply definition of Subset
130 ALL(b):[Subset(onlyX,b) <=> ALL(c):[c e onlyX => c e b]]
U Spec, 2
131 Subset(onlyX,sA) <=> ALL(c):[c e onlyX => c e sA]
U Spec, 130
132 [Subset(onlyX,sA) => ALL(c):[c e onlyX => c e sA]]
& [ALL(c):[c e onlyX => c e sA] => Subset(onlyX,sA)]
Iff-And, 131
133 Subset(onlyX,sA) => ALL(c):[c e onlyX => c e sA]
Split, 132
134 ALL(c):[c e onlyX => c e sA] => Subset(onlyX,sA)
Split, 132
Prove: ALL(c):[c e onlyX => c e sA]
Suppose...
135 z e onlyX
Premise
Apply definition of onlyX
136 z e onlyX <=> z e sA & z=x
U Spec, 129
137 [z e onlyX => z e sA & z=x]
& [z e sA & z=x => z e onlyX]
Iff-And, 136
138 z e onlyX => z e sA & z=x
Split, 137
139 z e sA & z=x => z e onlyX
Split, 137
140 z e sA & z=x
Detach, 138, 135
141 z e sA
Split, 140
As Required:
142 ALL(c):[c e onlyX => c e sA]
4 Conclusion, 135
143 Subset(onlyX,sA)
Detach, 134, 142
Apply definition of img
144 Subset(onlyX,sA) => Subset(img(onlyX),sB)
& ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]
U Spec, 7
145 Subset(img(onlyX),sB)
& ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]
Detach, 144, 143
146 Subset(img(onlyX),sB)
Split, 145
147 ALL(b):[b e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=b]]
Split, 145
Apply defintion of pre
148 Subset(img(onlyX),sB) => Subset(pre(img(onlyX)),sA)
& ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]
U Spec, 8
149 Subset(pre(img(onlyX)),sA)
& ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]
Detach, 148, 146
150 Subset(pre(img(onlyX)),sA)
Split, 149
151 ALL(b):[b e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(b)=c]]
Split, 149
152 y e pre(img(onlyX)) <=> EXIST(c):[c e img(onlyX) & f(y)=c]
U Spec, 151
153 [y e pre(img(onlyX)) => EXIST(c):[c e img(onlyX) & f(y)=c]]
& [EXIST(c):[c e img(onlyX) & f(y)=c] => y e pre(img(onlyX))]
Iff-And, 152
154 y e pre(img(onlyX)) => EXIST(c):[c e img(onlyX) & f(y)=c]
Split, 153
Sufficient: For y e pre(img(onlyX))
155 EXIST(c):[c e img(onlyX) & f(y)=c] => y e pre(img(onlyX))
Split, 153
Apply definition of onlyX
156 f(y) e img(onlyX) <=> EXIST(c):[c e onlyX & f(c)=f(y)]
U Spec, 147
157 [f(y) e img(onlyX) => EXIST(c):[c e onlyX & f(c)=f(y)]]
& [EXIST(c):[c e onlyX & f(c)=f(y)] => f(y) e img(onlyX)]
Iff-And, 156
158 f(y) e img(onlyX) => EXIST(c):[c e onlyX & f(c)=f(y)]
Split, 157
Sufficient: For f(y) e img(onlyX)
159 EXIST(c):[c e onlyX & f(c)=f(y)] => f(y) e img(onlyX)
Split, 157
160 x e onlyX <=> x e sA & x=x
U Spec, 129
161 [x e onlyX => x e sA & x=x]
& [x e sA & x=x => x e onlyX]
Iff-And, 160
162 x e onlyX => x e sA & x=x
Split, 161
163 x e sA & x=x => x e onlyX
Split, 161
164 x=x
Reflex
165 x e sA & x=x
Join, 121, 164
166 x e onlyX
Detach, 163, 165
167 x e onlyX & f(x)=f(y)
Join, 166, 124
168 EXIST(c):[c e onlyX & f(c)=f(y)]
E Gen, 167
169 f(y) e img(onlyX)
Detach, 159, 168
170 f(y)=f(y)
Reflex
171 f(y) e img(onlyX) & f(y)=f(y)
Join, 169, 170
172 EXIST(c):[c e img(onlyX) & f(y)=c]
E Gen, 171
173 y e pre(img(onlyX))
Detach, 155, 172
Apply definition of set equality
174 ALL(b):[onlyX=b <=> ALL(c):[c e onlyX <=> c e b]]
U Spec, 1
175 onlyX=pre(img(onlyX)) <=> ALL(c):[c e onlyX <=> c e pre(img(onlyX))]
U Spec, 174
176 [onlyX=pre(img(onlyX)) => ALL(c):[c e onlyX <=> c e pre(img(onlyX))]]
& [ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => onlyX=pre(img(onlyX))]
Iff-And, 175
177 onlyX=pre(img(onlyX)) => ALL(c):[c e onlyX <=> c e pre(img(onlyX))]
Split, 176
178 ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => onlyX=pre(img(onlyX))
Split, 176
179 ~ALL(c):[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))
Contra, 177
180 ~~EXIST(c):~[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))
Quant, 179
181 EXIST(c):~[c e onlyX <=> c e pre(img(onlyX))] => ~onlyX=pre(img(onlyX))
Rem DNeg, 180
182 EXIST(c):~[[c e onlyX => c e pre(img(onlyX))]
& [c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))
Iff-And, 181
183 EXIST(c):~~[~[c e onlyX => c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))
DeMorgan, 182
184 EXIST(c):[~[c e onlyX => c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))
Rem DNeg, 183
185 EXIST(c):[~~[c e onlyX & ~c e pre(img(onlyX))] | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))
Imply-And, 184
186 EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | ~[c e pre(img(onlyX)) => c e onlyX]] => ~onlyX=pre(img(onlyX))
Rem DNeg, 185
187 EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | ~~[c e pre(img(onlyX)) & ~c e onlyX]] => ~onlyX=pre(img(onlyX))
Imply-And, 186
Sufficient: For ~onlyX=pre(img(onlyX))
188 EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | c e pre(img(onlyX)) & ~c e onlyX] => ~onlyX=pre(img(onlyX))
Rem DNeg, 187
Apply definition of onlyX
189 y e onlyX <=> y e sA & y=x
U Spec, 129
190 [y e onlyX => y e sA & y=x]
& [y e sA & y=x => y e onlyX]
Iff-And, 189
191 y e onlyX => y e sA & y=x
Split, 190
192 y e sA & y=x => y e onlyX
Split, 190
193 ~[y e sA & y=x] => ~y e onlyX
Contra, 191
194 ~~[~y e sA | ~y=x] => ~y e onlyX
DeMorgan, 193
195 ~y e sA | ~y=x => ~y e onlyX
Rem DNeg, 194
196 ~y=x
Sym, 125
197 ~y e sA | ~y=x
Arb Or, 196
198 ~y e onlyX
Detach, 195, 197
199 y e pre(img(onlyX)) & ~y e onlyX
Join, 173, 198
200 y e onlyX & ~y e pre(img(onlyX)) | y e pre(img(onlyX)) & ~y e onlyX
Arb Or, 199
201 EXIST(c):[c e onlyX & ~c e pre(img(onlyX)) | c e pre(img(onlyX)) & ~c e onlyX]
E Gen, 200
202 ~onlyX=pre(img(onlyX))
Detach, 188, 201
203 Subset(onlyX,sA) & ~onlyX=pre(img(onlyX))
Join, 143, 202
204 EXIST(a):[Subset(a,sA) & ~a=pre(img(a))]
E Gen, 203
205 ~ALL(a):~[Subset(a,sA) & ~a=pre(img(a))]
Quant, 204
206 ~ALL(a):~~[Subset(a,sA) => ~~a=pre(img(a))]
Imply-And, 205
207 ~ALL(a):[Subset(a,sA) => ~~a=pre(img(a))]
Rem DNeg, 206
208 ~ALL(a):[Subset(a,sA) => a=pre(img(a))]
Rem DNeg, 207
As Required:
209 ~FOnto => ~ALL(a):[Subset(a,sA) => a=pre(img(a))]
4 Conclusion, 105
210 ~~ALL(a):[Subset(a,sA) => a=pre(img(a))] => ~~FOnto
Contra, 209
211 ALL(a):[Subset(a,sA) => a=pre(img(a))] => ~~FOnto
Rem DNeg, 210
212 ALL(a):[Subset(a,sA) => a=pre(img(a))] => FOnto
Rem DNeg, 211
213 [ALL(a):[Subset(a,sA) => a=pre(img(a))] => FOnto]
& [FOnto => ALL(a):[Subset(a,sA) => a=pre(img(a))]]
Join, 212, 104
As Required:
214 ALL(a):[Subset(a,sA) => a=pre(img(a))] <=> FOnto
Iff-And, 213