LEMMA 2
*******
Suppose we have injective f: x --> y.
Then there exists bijective g: x --> f[x] (the image of x under f).
(This proof was written with aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
OUTLINE
*******
Suppose an injective (one-to-one) function f maps set x to set y.
Construct the subset imgf of y, the image set of x under f (i.e. the range of f).
Construct the function g, a simple restriction of f to its image set imgf.
Prove g is bijective.
DEFINITIONS
***********
Define: Injection
1 ALL(f):ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
Axiom
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
Define: Bijection
3 ALL(f):ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]
Axiom
PROOF OF LEMMA 2
****************
Suppose an injective (one-to-one) function f maps set x to set y
4 Set(x)
& Set(y)
& ALL(c):[c e x => f(c) e y]
& Injection(f,x,y)
Premise
5 Set(x)
Split, 4
6 Set(y)
Split, 4
7 ALL(c):[c e x => f(c) e y]
Split, 4
8 Injection(f,x,y)
Split, 4
Apply definition of Injection
9 ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [f(c)=f(d) => c=d]]]
U Spec, 1
10 ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 9
11 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 10
12 [Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)]
Iff-And, 11
13 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 12
14 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)
Split, 12
15 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 13, 8
Construct the subset imgf of y, the image set of x under f (the range of f).
Apply the Subset Axiom.
16 EXIST(sub):[Set(sub) & ALL(d):[d e sub <=> d e y & EXIST(e):[e e x & f(e)=d]]]
Subset, 6
17 Set(imgf) & ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
E Spec, 16
Define: imgf (the image set of x under f, i.e. the range of f)
************
18 Set(imgf)
Split, 17
19 ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
Split, 17
Construct the function g.
Apply Cartesian Product Axiom.
20 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
21 ALL(a2):[Set(x) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e a2]]]
U Spec, 20
22 Set(x) & Set(imgf) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e imgf]]
U Spec, 21
23 Set(x) & Set(imgf)
Join, 5, 18
24 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e imgf]]
Detach, 22, 23
25 Set'(ximgf) & ALL(c1):ALL(c2):[(c1,c2) e ximgf <=> c1 e x & c2 e imgf]
E Spec, 24
Define: ximgf (the Cartesian product of sets x and imgf)
*************
26 Set'(ximgf)
Split, 25
27 ALL(c1):ALL(c2):[(c1,c2) e ximgf <=> c1 e x & c2 e imgf]
Split, 25
Apply Subset Axiom
28 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e ximgf & b=f(a)]]
Subset, 26
29 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e ximgf & b=f(a)]
E Spec, 28
Define: g
*********
30 Set'(g)
Split, 29
31 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e ximgf & b=f(a)]
Split, 29
Prove: g is a function
Apply Function Axiom
32 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
33 ALL(a):ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e a & d e b]
& ALL(c):[c e a => EXIST(d):[d e b & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]
U Spec, 32
34 ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e x & d e b]
& ALL(c):[c e x => EXIST(d):[d e b & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]]
U Spec, 33
Sufficient: For functionality of g
35 ALL(c):ALL(d):[(c,d) e g => c e x & d e imgf]
& ALL(c):[c e x => EXIST(d):[d e imgf & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
=> ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]
U Spec, 34
Prove: ALL(c):ALL(d):[(c,d) e g => c e x & d e imgf]
Suppose...
36 (t,u) e g
Premise
Apply definition of g
37 ALL(b):[(t,b) e g <=> (t,b) e ximgf & b=f(t)]
U Spec, 31
38 (t,u) e g <=> (t,u) e ximgf & u=f(t)
U Spec, 37
39 [(t,u) e g => (t,u) e ximgf & u=f(t)]
& [(t,u) e ximgf & u=f(t) => (t,u) e g]
Iff-And, 38
40 (t,u) e g => (t,u) e ximgf & u=f(t)
Split, 39
41 (t,u) e ximgf & u=f(t) => (t,u) e g
Split, 39
42 (t,u) e ximgf & u=f(t)
Detach, 40, 36
43 (t,u) e ximgf
Split, 42
44 u=f(t)
Split, 42
Apply definition of ximgf
45 ALL(c2):[(t,c2) e ximgf <=> t e x & c2 e imgf]
U Spec, 27
46 (t,u) e ximgf <=> t e x & u e imgf
U Spec, 45
47 [(t,u) e ximgf => t e x & u e imgf]
& [t e x & u e imgf => (t,u) e ximgf]
Iff-And, 46
48 (t,u) e ximgf => t e x & u e imgf
Split, 47
49 t e x & u e imgf => (t,u) e ximgf
Split, 47
50 t e x & u e imgf
Detach, 48, 43
Functionality, Part 1
51 ALL(c):ALL(d):[(c,d) e g => c e x & d e imgf]
4 Conclusion, 36
Prove: ALL(c):[c e x => EXIST(d):[d e imgf & (c,d) e g]]
Suppose...
52 t e x
Premise
Apply definition of g
53 ALL(b):[(t,b) e g <=> (t,b) e ximgf & b=f(t)]
U Spec, 31
54 (t,f(t)) e g <=> (t,f(t)) e ximgf & f(t)=f(t)
U Spec, 53
55 [(t,f(t)) e g => (t,f(t)) e ximgf & f(t)=f(t)]
& [(t,f(t)) e ximgf & f(t)=f(t) => (t,f(t)) e g]
Iff-And, 54
56 (t,f(t)) e g => (t,f(t)) e ximgf & f(t)=f(t)
Split, 55
Sufficient: (t,f(t)) e g
57 (t,f(t)) e ximgf & f(t)=f(t) => (t,f(t)) e g
Split, 55
Apply definition of ximgf
58 ALL(c2):[(t,c2) e ximgf <=> t e x & c2 e imgf]
U Spec, 27
59 (t,f(t)) e ximgf <=> t e x & f(t) e imgf
U Spec, 58
60 [(t,f(t)) e ximgf => t e x & f(t) e imgf]
& [t e x & f(t) e imgf => (t,f(t)) e ximgf]
Iff-And, 59
61 (t,f(t)) e ximgf => t e x & f(t) e imgf
Split, 60
Sufficient: (t,f(t)) e ximgf
62 t e x & f(t) e imgf => (t,f(t)) e ximgf
Split, 60
Apply definition of imgf
63 f(t) e imgf <=> f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
U Spec, 19
64 [f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]]
& [f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf]
Iff-And, 63
65 f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Split, 64
Sufficient: f(t) e imgf
66 f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf
Split, 64
Apply definition of f
67 t e x => f(t) e y
U Spec, 7
68 f(t) e y
Detach, 67, 52
69 f(t)=f(t)
Reflex
70 t e x & f(t)=f(t)
Join, 52, 69
71 EXIST(e):[e e x & f(e)=f(t)]
E Gen, 70
72 f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Join, 68, 71
73 f(t) e imgf
Detach, 66, 72
74 t e x & f(t) e imgf
Join, 52, 73
75 (t,f(t)) e ximgf
Detach, 62, 74
76 (t,f(t)) e ximgf & f(t)=f(t)
Join, 75, 69
77 (t,f(t)) e g
Detach, 57, 76
78 f(t) e imgf & (t,f(t)) e g
Join, 73, 77
79 EXIST(d):[d e imgf & (t,d) e g]
E Gen, 78
Functionality, Part 2
80 ALL(c):[c e x => EXIST(d):[d e imgf & (c,d) e g]]
4 Conclusion, 52
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Suppose...
81 (t,u1) e g & (t,u2) e g
Premise
82 (t,u1) e g
Split, 81
83 (t,u2) e g
Split, 81
Apply definition of g
84 ALL(b):[(t,b) e g <=> (t,b) e ximgf & b=f(t)]
U Spec, 31
85 (t,u1) e g <=> (t,u1) e ximgf & u1=f(t)
U Spec, 84
86 [(t,u1) e g => (t,u1) e ximgf & u1=f(t)]
& [(t,u1) e ximgf & u1=f(t) => (t,u1) e g]
Iff-And, 85
87 (t,u1) e g => (t,u1) e ximgf & u1=f(t)
Split, 86
88 (t,u1) e ximgf & u1=f(t) => (t,u1) e g
Split, 86
89 (t,u1) e ximgf & u1=f(t)
Detach, 87, 82
90 (t,u1) e ximgf
Split, 89
91 u1=f(t)
Split, 89
Apply definition of g
92 (t,u2) e g <=> (t,u2) e ximgf & u2=f(t)
U Spec, 84
93 [(t,u2) e g => (t,u2) e ximgf & u2=f(t)]
& [(t,u2) e ximgf & u2=f(t) => (t,u2) e g]
Iff-And, 92
94 (t,u2) e g => (t,u2) e ximgf & u2=f(t)
Split, 93
95 (t,u2) e ximgf & u2=f(t) => (t,u2) e g
Split, 93
96 (t,u2) e ximgf & u2=f(t)
Detach, 94, 83
97 (t,u2) e ximgf
Split, 96
98 u2=f(t)
Split, 96
99 u1=u2
Substitute, 98, 91
Functionality, Part 3
100 ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
4 Conclusion, 81
Joining results...
101 ALL(c):ALL(d):[(c,d) e g => c e x & d e imgf]
& ALL(c):[c e x => EXIST(d):[d e imgf & (c,d) e g]]
Join, 51, 80
102 ALL(c):ALL(d):[(c,d) e g => c e x & d e imgf]
& ALL(c):[c e x => EXIST(d):[d e imgf & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Join, 101, 100
As Required: g is a function
103 ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]
Detach, 35, 102
Prove: ALL(d):[d e x => g(d) e imgf]
Suppose...
104 t e x
Premise
Apply functionality of g
105 t e x => EXIST(d):[d e imgf & (t,d) e g]
U Spec, 80
106 EXIST(d):[d e imgf & (t,d) e g]
Detach, 105, 104
107 u e imgf & (t,u) e g
E Spec, 106
108 u e imgf
Split, 107
109 (t,u) e g
Split, 107
Apply functionality of g
110 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 103
111 u=g(t) <=> (t,u) e g
U Spec, 110
112 [u=g(t) => (t,u) e g] & [(t,u) e g => u=g(t)]
Iff-And, 111
113 u=g(t) => (t,u) e g
Split, 112
114 (t,u) e g => u=g(t)
Split, 112
115 u=g(t)
Detach, 114, 109
116 g(t) e imgf
Substitute, 115, 108
As Required:
117 ALL(d):[d e x => g(d) e imgf]
4 Conclusion, 104
Prove: ALL(d):[d e x => g(d)=f(d)]
Suppose...
118 t e x
Premise
Apply definition of g
119 ALL(b):[(t,b) e g <=> (t,b) e ximgf & b=f(t)]
U Spec, 31
120 (t,f(t)) e g <=> (t,f(t)) e ximgf & f(t)=f(t)
U Spec, 119
121 [(t,f(t)) e g => (t,f(t)) e ximgf & f(t)=f(t)]
& [(t,f(t)) e ximgf & f(t)=f(t) => (t,f(t)) e g]
Iff-And, 120
122 (t,f(t)) e g => (t,f(t)) e ximgf & f(t)=f(t)
Split, 121
Sufficient: (t,f(t)) e g
123 (t,f(t)) e ximgf & f(t)=f(t) => (t,f(t)) e g
Split, 121
Apply definition of ximgf
124 ALL(c2):[(t,c2) e ximgf <=> t e x & c2 e imgf]
U Spec, 27
125 (t,f(t)) e ximgf <=> t e x & f(t) e imgf
U Spec, 124
126 [(t,f(t)) e ximgf => t e x & f(t) e imgf]
& [t e x & f(t) e imgf => (t,f(t)) e ximgf]
Iff-And, 125
127 (t,f(t)) e ximgf => t e x & f(t) e imgf
Split, 126
Sufficient: (t,f(t)) e ximgf
128 t e x & f(t) e imgf => (t,f(t)) e ximgf
Split, 126
Apply definition of imgf
129 f(t) e imgf <=> f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
U Spec, 19
130 [f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]]
& [f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf]
Iff-And, 129
131 f(t) e imgf => f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Split, 130
Sufficient: f(t) e imgf
132 f(t) e y & EXIST(e):[e e x & f(e)=f(t)] => f(t) e imgf
Split, 130
Apply definition of f
133 t e x => f(t) e y
U Spec, 7
134 f(t) e y
Detach, 133, 118
135 f(t)=f(t)
Reflex
136 t e x & f(t)=f(t)
Join, 118, 135
137 EXIST(e):[e e x & f(e)=f(t)]
E Gen, 136
138 f(t) e y & EXIST(e):[e e x & f(e)=f(t)]
Join, 134, 137
139 f(t) e imgf
Detach, 132, 138
140 t e x & f(t) e imgf
Join, 118, 139
141 (t,f(t)) e ximgf
Detach, 128, 140
142 (t,f(t)) e ximgf & f(t)=f(t)
Join, 141, 135
143 (t,f(t)) e g
Detach, 123, 142
Apply functionality of g
144 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 103
145 f(t)=g(t) <=> (t,f(t)) e g
U Spec, 144
146 [f(t)=g(t) => (t,f(t)) e g]
& [(t,f(t)) e g => f(t)=g(t)]
Iff-And, 145
147 f(t)=g(t) => (t,f(t)) e g
Split, 146
148 (t,f(t)) e g => f(t)=g(t)
Split, 146
149 f(t)=g(t)
Detach, 148, 143
150 g(t)=f(t)
Sym, 149
As Required:
151 ALL(d):[d e x => g(d)=f(d)]
4 Conclusion, 118
Prove: Bijection(g,x,imgf)
Apply definition of Bijection
152 ALL(a):ALL(b):[Bijection(g,a,b) <=> Injection(g,a,b) & Surjection(g,a,b)]
U Spec, 3
153 ALL(b):[Bijection(g,x,b) <=> Injection(g,x,b) & Surjection(g,x,b)]
U Spec, 152
154 Bijection(g,x,imgf) <=> Injection(g,x,imgf) & Surjection(g,x,imgf)
U Spec, 153
155 [Bijection(g,x,imgf) => Injection(g,x,imgf) & Surjection(g,x,imgf)]
& [Injection(g,x,imgf) & Surjection(g,x,imgf) => Bijection(g,x,imgf)]
Iff-And, 154
156 Bijection(g,x,imgf) => Injection(g,x,imgf) & Surjection(g,x,imgf)
Split, 155
Sufficient: Bijection(g,x,imgf)
157 Injection(g,x,imgf) & Surjection(g,x,imgf) => Bijection(g,x,imgf)
Split, 155
Prove: Injection(g,x,imgf)
Apply definition of Injection
158 ALL(a):ALL(b):[Injection(g,a,b) <=> ALL(c):ALL(d):[c e a & d e a => [g(c)=g(d) => c=d]]]
U Spec, 1
159 ALL(b):[Injection(g,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]]
U Spec, 158
160 Injection(g,x,imgf) <=> ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]
U Spec, 159
161 [Injection(g,x,imgf) => ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]]
& [ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]] => Injection(g,x,imgf)]
Iff-And, 160
162 Injection(g,x,imgf) => ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]
Split, 161
Sufficient: Injection(g,x,imgf)
163 ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]] => Injection(g,x,imgf)
Split, 161
Prove: ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]
Suppose...
164 t1 e x & t2 e x
Premise
165 t1 e x
Split, 164
166 t2 e x
Split, 164
Prove: g(t1)=g(t2) => t1=t2
Suppose...
167 g(t1)=g(t2)
Premise
Apply definition of g
168 t1 e x => g(t1)=f(t1)
U Spec, 151
169 g(t1)=f(t1)
Detach, 168, 165
Apply definition of g
170 t2 e x => g(t2)=f(t2)
U Spec, 151
171 g(t2)=f(t2)
Detach, 170, 166
172 f(t1)=g(t2)
Substitute, 169, 167
173 f(t1)=f(t2)
Substitute, 171, 172
Apply definition of f
174 ALL(d):[t1 e x & d e x => [f(t1)=f(d) => t1=d]]
U Spec, 15
175 t1 e x & t2 e x => [f(t1)=f(t2) => t1=t2]
U Spec, 174
176 f(t1)=f(t2) => t1=t2
Detach, 175, 164
177 t1=t2
Detach, 176, 173
As Required:
178 g(t1)=g(t2) => t1=t2
4 Conclusion, 167
As Required:
179 ALL(c):ALL(d):[c e x & d e x => [g(c)=g(d) => c=d]]
4 Conclusion, 164
As Required:
180 Injection(g,x,imgf)
Detach, 163, 179
Prove: Surjection(g,x,imgf)
Apply definition of Surjection
181 ALL(a):ALL(b):[Surjection(g,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]
U Spec, 2
182 ALL(b):[Surjection(g,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & g(d)=c]]]
U Spec, 181
183 Surjection(g,x,imgf) <=> ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]]
U Spec, 182
184 [Surjection(g,x,imgf) => ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]]]
& [ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]] => Surjection(g,x,imgf)]
Iff-And, 183
185 Surjection(g,x,imgf) => ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]]
Split, 184
Sufficient: Surjection(g,x,imgf)
186 ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]] => Surjection(g,x,imgf)
Split, 184
Prove: ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]]
Suppose...
187 t e imgf
Premise
Apply definition of imgf
188 t e imgf <=> t e y & EXIST(e):[e e x & f(e)=t]
U Spec, 19
189 [t e imgf => t e y & EXIST(e):[e e x & f(e)=t]]
& [t e y & EXIST(e):[e e x & f(e)=t] => t e imgf]
Iff-And, 188
190 t e imgf => t e y & EXIST(e):[e e x & f(e)=t]
Split, 189
191 t e y & EXIST(e):[e e x & f(e)=t] => t e imgf
Split, 189
192 t e y & EXIST(e):[e e x & f(e)=t]
Detach, 190, 187
193 t e y
Split, 192
194 EXIST(e):[e e x & f(e)=t]
Split, 192
195 u e x & f(u)=t
E Spec, 194
196 u e x
Split, 195
197 f(u)=t
Split, 195
198 u e x => g(u)=f(u)
U Spec, 151
199 g(u)=f(u)
Detach, 198, 196
200 g(u)=t
Substitute, 199, 197
201 u e x & g(u)=t
Join, 196, 200
202 EXIST(d):[d e x & g(d)=t]
E Gen, 201
As Required:
203 ALL(c):[c e imgf => EXIST(d):[d e x & g(d)=c]]
4 Conclusion, 187
As Required:
204 Surjection(g,x,imgf)
Detach, 186, 203
Joining results...
205 Injection(g,x,imgf) & Surjection(g,x,imgf)
Join, 180, 204
As Required:
206 Bijection(g,x,imgf)
Detach, 157, 205
Joining results...
207 Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
Join, 18, 19
208 Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e imgf]
Join, 207, 117
209 Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e imgf]
& ALL(d):[d e x => g(d)=f(d)]
Join, 208, 151
210 Set(imgf)
& ALL(d):[d e imgf <=> d e y & EXIST(e):[e e x & f(e)=d]]
& ALL(d):[d e x => g(d) e imgf]
& ALL(d):[d e x => g(d)=f(d)]
& Bijection(g,x,imgf)
Join, 209, 206
As Required:
211 ALL(a):ALL(b):ALL(f):[Set(a)
& Set(b)
& ALL(c):[c e a => f(c) e b]
& Injection(f,a,b)
=> EXIST(c):EXIST(g):[Set(c)
& ALL(d):[d e c <=> d e b & EXIST(e):[e e a & f(e)=d]]
& ALL(d):[d e a => g(d) e c]
& ALL(d):[d e a => g(d)=f(d)]
& Bijection(g,a,c)]]
4 Conclusion, 4