LEMMA 1
*******
Every bijection has an inverse that is itself a bijection.
(This proof was written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com )
OUTLINE
*******
Suppose f is a function mapping set x to set y.
Suppose further that f is a bijection.
Construct set of ordered pairs g (reversing the co-ordinates of f).
Prove g is a bijection.
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 1
****************
Suppose f is a function mapping set x to set y
4 Set(x) & Set(y) & ALL(c):[c e x => f(c) e y]
Premise
5 Set(x)
Split, 4
6 Set(y)
Split, 4
7 ALL(c):[c e x => f(c) e y]
Split, 4
Suppose f is a bijection
8 Bijection(f,x,y)
Premise
Apply definition of Bijection
9 ALL(a):ALL(b):[Bijection(f,a,b) <=> Injection(f,a,b) & Surjection(f,a,b)]
U Spec, 3
10 ALL(b):[Bijection(f,x,b) <=> Injection(f,x,b) & Surjection(f,x,b)]
U Spec, 9
11 Bijection(f,x,y) <=> Injection(f,x,y) & Surjection(f,x,y)
U Spec, 10
12 [Bijection(f,x,y) => Injection(f,x,y) & Surjection(f,x,y)]
& [Injection(f,x,y) & Surjection(f,x,y) => Bijection(f,x,y)]
Iff-And, 11
13 Bijection(f,x,y) => Injection(f,x,y) & Surjection(f,x,y)
Split, 12
14 Injection(f,x,y) & Surjection(f,x,y) => Bijection(f,x,y)
Split, 12
15 Injection(f,x,y) & Surjection(f,x,y)
Detach, 13, 8
16 Injection(f,x,y)
Split, 15
17 Surjection(f,x,y)
Split, 15
Apply definition of Injection
18 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
19 ALL(b):[Injection(f,x,b) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]]
U Spec, 18
20 Injection(f,x,y) <=> ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
U Spec, 19
21 [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, 20
22 Injection(f,x,y) => ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Split, 21
23 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]] => Injection(f,x,y)
Split, 21
24 ALL(c):ALL(d):[c e x & d e x => [f(c)=f(d) => c=d]]
Detach, 22, 16
Apply definition of Surjection
25 ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]
U Spec, 2
26 ALL(b):[Surjection(f,x,b) <=> ALL(c):[c e b => EXIST(d):[d e x & f(d)=c]]]
U Spec, 25
27 Surjection(f,x,y) <=> ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]]
U Spec, 26
28 [Surjection(f,x,y) => ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]]]
& [ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]] => Surjection(f,x,y)]
Iff-And, 27
29 Surjection(f,x,y) => ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]]
Split, 28
30 ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]] => Surjection(f,x,y)
Split, 28
31 ALL(c):[c e y => EXIST(d):[d e x & f(d)=c]]
Detach, 29, 17
Construct function g, the inverse of f.
Apply the Cartesian Product Axiom.
32 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
33 ALL(a2):[Set(y) & Set(a2) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e a2]]]
U Spec, 32
34 Set(y) & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
U Spec, 33
35 Set(y) & Set(x)
Join, 6, 5
36 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e y & c2 e x]]
Detach, 34, 35
37 Set'(yx) & ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
E Spec, 36
Define: yx (Cartesian product of sets y and x)
38 Set'(yx)
Split, 37
39 ALL(c1):ALL(c2):[(c1,c2) e yx <=> c1 e y & c2 e x]
Split, 37
Construct g
Apply Subset Axiom
40 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e yx & a=f(b)]]
Subset, 38
41 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e yx & a=f(b)]
E Spec, 40
Define: g (the inverse of f)
42 Set'(g)
Split, 41
43 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e yx & a=f(b)]
Split, 41
Prove functionality of g
Apply Function Axiom
44 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
45 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, 44
46 ALL(b):[ALL(c):ALL(d):[(c,d) e g => c e y & d e b]
& ALL(c):[c e y => 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, 45
Sufficient: For functionality of g
47 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (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, 46
Prove: ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
Suppose...
48 (t,u) e g
Premise
Apply definition of g
49 ALL(b):[(t,b) e g <=> (t,b) e yx & t=f(b)]
U Spec, 43
50 (t,u) e g <=> (t,u) e yx & t=f(u)
U Spec, 49
51 [(t,u) e g => (t,u) e yx & t=f(u)]
& [(t,u) e yx & t=f(u) => (t,u) e g]
Iff-And, 50
52 (t,u) e g => (t,u) e yx & t=f(u)
Split, 51
53 (t,u) e yx & t=f(u) => (t,u) e g
Split, 51
54 (t,u) e yx & t=f(u)
Detach, 52, 48
55 (t,u) e yx
Split, 54
56 t=f(u)
Split, 54
Apply definition of yx
57 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 39
58 (t,u) e yx <=> t e y & u e x
U Spec, 57
59 [(t,u) e yx => t e y & u e x]
& [t e y & u e x => (t,u) e yx]
Iff-And, 58
60 (t,u) e yx => t e y & u e x
Split, 59
61 t e y & u e x => (t,u) e yx
Split, 59
62 t e y & u e x
Detach, 60, 55
Functionality, Part 1
63 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
4 Conclusion, 48
Prove: ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
Suppose...
64 t e y
Premise
Apply previous result
65 t e y => EXIST(d):[d e x & f(d)=t]
U Spec, 31
66 EXIST(d):[d e x & f(d)=t]
Detach, 65, 64
67 u e x & f(u)=t
E Spec, 66
68 u e x
Split, 67
69 f(u)=t
Split, 67
Apply definition of g
70 ALL(b):[(t,b) e g <=> (t,b) e yx & t=f(b)]
U Spec, 43
71 (t,u) e g <=> (t,u) e yx & t=f(u)
U Spec, 70
72 [(t,u) e g => (t,u) e yx & t=f(u)]
& [(t,u) e yx & t=f(u) => (t,u) e g]
Iff-And, 71
73 (t,u) e g => (t,u) e yx & t=f(u)
Split, 72
Sufficient: (t,u) e g
74 (t,u) e yx & t=f(u) => (t,u) e g
Split, 72
Apply definition of yx
75 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 39
76 (t,u) e yx <=> t e y & u e x
U Spec, 75
77 [(t,u) e yx => t e y & u e x]
& [t e y & u e x => (t,u) e yx]
Iff-And, 76
78 (t,u) e yx => t e y & u e x
Split, 77
79 t e y & u e x => (t,u) e yx
Split, 77
80 t e y & u e x
Join, 64, 68
81 (t,u) e yx
Detach, 79, 80
82 t=f(u)
Sym, 69
83 (t,u) e yx & t=f(u)
Join, 81, 82
84 (t,u) e g
Detach, 74, 83
85 u e x & (t,u) e g
Join, 68, 84
86 EXIST(d):[d e x & (t,d) e g]
E Gen, 85
Functionality, Part 2
87 ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
4 Conclusion, 64
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Suppose...
88 (t,u1) e g & (t,u2) e g
Premise
89 (t,u1) e g
Split, 88
90 (t,u2) e g
Split, 88
Apply definition of g
91 ALL(b):[(t,b) e g <=> (t,b) e yx & t=f(b)]
U Spec, 43
92 (t,u1) e g <=> (t,u1) e yx & t=f(u1)
U Spec, 91
93 [(t,u1) e g => (t,u1) e yx & t=f(u1)]
& [(t,u1) e yx & t=f(u1) => (t,u1) e g]
Iff-And, 92
94 (t,u1) e g => (t,u1) e yx & t=f(u1)
Split, 93
95 (t,u1) e yx & t=f(u1) => (t,u1) e g
Split, 93
96 (t,u1) e yx & t=f(u1)
Detach, 94, 89
97 (t,u1) e yx
Split, 96
98 t=f(u1)
Split, 96
Apply definition of g
99 (t,u2) e g <=> (t,u2) e yx & t=f(u2)
U Spec, 91
100 [(t,u2) e g => (t,u2) e yx & t=f(u2)]
& [(t,u2) e yx & t=f(u2) => (t,u2) e g]
Iff-And, 99
101 (t,u2) e g => (t,u2) e yx & t=f(u2)
Split, 100
102 (t,u2) e yx & t=f(u2) => (t,u2) e g
Split, 100
103 (t,u2) e yx & t=f(u2)
Detach, 101, 90
104 (t,u2) e yx
Split, 103
105 t=f(u2)
Split, 103
106 f(u1)=f(u2)
Substitute, 98, 105
Apply injectivity of f
107 ALL(d):[u1 e x & d e x => [f(u1)=f(d) => u1=d]]
U Spec, 24
108 u1 e x & u2 e x => [f(u1)=f(u2) => u1=u2]
U Spec, 107
Apply definition of yx
109 ALL(c2):[(t,c2) e yx <=> t e y & c2 e x]
U Spec, 39
110 (t,u1) e yx <=> t e y & u1 e x
U Spec, 109
111 [(t,u1) e yx => t e y & u1 e x]
& [t e y & u1 e x => (t,u1) e yx]
Iff-And, 110
112 (t,u1) e yx => t e y & u1 e x
Split, 111
113 t e y & u1 e x => (t,u1) e yx
Split, 111
114 t e y & u1 e x
Detach, 112, 97
115 t e y
Split, 114
116 u1 e x
Split, 114
Apply definition of yx
117 (t,u2) e yx <=> t e y & u2 e x
U Spec, 109
118 [(t,u2) e yx => t e y & u2 e x]
& [t e y & u2 e x => (t,u2) e yx]
Iff-And, 117
119 (t,u2) e yx => t e y & u2 e x
Split, 118
120 t e y & u2 e x => (t,u2) e yx
Split, 118
121 t e y & u2 e x
Detach, 119, 104
122 t e y
Split, 121
123 u2 e x
Split, 121
124 u1 e x & u2 e x
Join, 116, 123
125 f(u1)=f(u2) => u1=u2
Detach, 108, 124
126 u1=u2
Detach, 125, 106
Functionality, Part 3
127 ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
4 Conclusion, 88
128 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
Join, 63, 87
129 ALL(c):ALL(d):[(c,d) e g => c e y & d e x]
& ALL(c):[c e y => EXIST(d):[d e x & (c,d) e g]]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e g & (c,d2) e g => d1=d2]
Join, 128, 127
As Required:
g is a function
130 ALL(c):ALL(d):[d=g(c) <=> (c,d) e g]
Detach, 47, 129
Prove: ALL(a):[a e y => g(a) e x]
Suppose...
131 t e y
Premise
Apply functionality of g
132 t e y => EXIST(d):[d e x & (t,d) e g]
U Spec, 87
133 EXIST(d):[d e x & (t,d) e g]
Detach, 132, 131
134 u e x & (t,u) e g
E Spec, 133
135 u e x
Split, 134
136 (t,u) e g
Split, 134
Apply functionality of g
137 ALL(d):[d=g(t) <=> (t,d) e g]
U Spec, 130
138 u=g(t) <=> (t,u) e g
U Spec, 137
139 [u=g(t) => (t,u) e g] & [(t,u) e g => u=g(t)]
Iff-And, 138
140 u=g(t) => (t,u) e g
Split, 139
141 (t,u) e g => u=g(t)
Split, 139
142 u=g(t)
Detach, 141, 136
143 g(t) e x
Substitute, 142, 135
As Required:
144 ALL(a):[a e y => g(a) e x]
4 Conclusion, 131
145 ALL(c):[c e y => g(c) e x]
Rename, 144
Prove g is the inverse of f
Suppose...
146 t e x & u e y
Premise
147 t e x
Split, 146
148 u e y
Split, 146
'=>'
Prove: f(t)=u => g(u)=t
Suppose...
149 f(t)=u
Premise
Apply definition of g
150 ALL(b):[(u,b) e g <=> (u,b) e yx & u=f(b)]
U Spec, 43
151 (u,t) e g <=> (u,t) e yx & u=f(t)
U Spec, 150
152 [(u,t) e g => (u,t) e yx & u=f(t)]
& [(u,t) e yx & u=f(t) => (u,t) e g]
Iff-And, 151
153 (u,t) e g => (u,t) e yx & u=f(t)
Split, 152
154 (u,t) e yx & u=f(t) => (u,t) e g
Split, 152
Apply definition of yx
155 ALL(c2):[(u,c2) e yx <=> u e y & c2 e x]
U Spec, 39
156 (u,t) e yx <=> u e y & t e x
U Spec, 155
157 [(u,t) e yx => u e y & t e x]
& [u e y & t e x => (u,t) e yx]
Iff-And, 156
158 (u,t) e yx => u e y & t e x
Split, 157
159 u e y & t e x => (u,t) e yx
Split, 157
160 u e y & t e x
Join, 148, 147
161 (u,t) e yx
Detach, 159, 160
162 u=f(t)
Sym, 149
163 (u,t) e yx & u=f(t)
Join, 161, 162
164 (u,t) e g
Detach, 154, 163
Apply functionality of g
165 ALL(d):[d=g(u) <=> (u,d) e g]
U Spec, 130
166 t=g(u) <=> (u,t) e g
U Spec, 165
167 [t=g(u) => (u,t) e g] & [(u,t) e g => t=g(u)]
Iff-And, 166
168 t=g(u) => (u,t) e g
Split, 167
169 (u,t) e g => t=g(u)
Split, 167
170 t=g(u)
Detach, 169, 164
171 g(u)=t
Sym, 170
As Required:
172 f(t)=u => g(u)=t
4 Conclusion, 149
'<='
Prove: g(u)=t => f(t)=u
Suppose...
173 g(u)=t
Premise
Apply functionality of g
174 ALL(d):[d=g(u) <=> (u,d) e g]
U Spec, 130
175 t=g(u) <=> (u,t) e g
U Spec, 174
176 [t=g(u) => (u,t) e g] & [(u,t) e g => t=g(u)]
Iff-And, 175
177 t=g(u) => (u,t) e g
Split, 176
178 (u,t) e g => t=g(u)
Split, 176
179 t=g(u)
Sym, 173
180 (u,t) e g
Detach, 177, 179
Apply definition of g
181 ALL(b):[(u,b) e g <=> (u,b) e yx & u=f(b)]
U Spec, 43
182 (u,t) e g <=> (u,t) e yx & u=f(t)
U Spec, 181
183 [(u,t) e g => (u,t) e yx & u=f(t)]
& [(u,t) e yx & u=f(t) => (u,t) e g]
Iff-And, 182
184 (u,t) e g => (u,t) e yx & u=f(t)
Split, 183
185 (u,t) e yx & u=f(t) => (u,t) e g
Split, 183
186 (u,t) e yx & u=f(t)
Detach, 184, 180
187 (u,t) e yx
Split, 186
188 u=f(t)
Split, 186
189 f(t)=u
Sym, 188
As Required:
190 g(u)=t => f(t)=u
4 Conclusion, 173
191 [g(u)=t => f(t)=u] & [f(t)=u => g(u)=t]
Join, 190, 172
192 g(u)=t <=> f(t)=u
Iff-And, 191
As Required:
g is the inverse of f
193 ALL(a):ALL(b):[a e x & b e y => [g(b)=a <=> f(a)=b]]
4 Conclusion, 146
194 ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]
Rename, 193
Apply definition of Bijection
195 ALL(a):ALL(b):[Bijection(g,a,b) <=> Injection(g,a,b) & Surjection(g,a,b)]
U Spec, 3
196 ALL(b):[Bijection(g,y,b) <=> Injection(g,y,b) & Surjection(g,y,b)]
U Spec, 195
197 Bijection(g,y,x) <=> Injection(g,y,x) & Surjection(g,y,x)
U Spec, 196
198 [Bijection(g,y,x) => Injection(g,y,x) & Surjection(g,y,x)]
& [Injection(g,y,x) & Surjection(g,y,x) => Bijection(g,y,x)]
Iff-And, 197
199 Bijection(g,y,x) => Injection(g,y,x) & Surjection(g,y,x)
Split, 198
Sufficient: Bijection(g,y,x)
200 Injection(g,y,x) & Surjection(g,y,x) => Bijection(g,y,x)
Split, 198
Apply definition of Injection
201 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
202 ALL(b):[Injection(g,y,b) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]
U Spec, 201
203 Injection(g,y,x) <=> ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
U Spec, 202
204 [Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]]
& [ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)]
Iff-And, 203
205 Injection(g,y,x) => ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
Split, 204
Sufficient: Injection(g,y,x)
206 ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]] => Injection(g,y,x)
Split, 204
Prove: ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
Suppose...
207 t e y & u e y
Premise
208 t e y
Split, 207
209 u e y
Split, 207
Prove: g(t)=g(u) => t=u
Suppose...
210 g(t)=g(u)
Premise
Apply previous result
211 ALL(b):[g(u) e x & b e y => [g(b)=g(u) <=> f(g(u))=b]]
U Spec, 193
212 g(u) e x & t e y => [g(t)=g(u) <=> f(g(u))=t]
U Spec, 211
213 g(u) e x & u e y => [g(u)=g(u) <=> f(g(u))=u]
U Spec, 211
214 u e y => g(u) e x
U Spec, 144
215 g(u) e x
Detach, 214, 209
216 g(u) e x & t e y
Join, 215, 208
217 g(t)=g(u) <=> f(g(u))=t
Detach, 212, 216
218 [g(t)=g(u) => f(g(u))=t] & [f(g(u))=t => g(t)=g(u)]
Iff-And, 217
219 g(t)=g(u) => f(g(u))=t
Split, 218
220 f(g(u))=t => g(t)=g(u)
Split, 218
221 f(g(u))=t
Detach, 219, 210
222 g(u) e x & u e y
Join, 215, 209
223 g(u)=g(u) <=> f(g(u))=u
Detach, 213, 222
224 [g(u)=g(u) => f(g(u))=u] & [f(g(u))=u => g(u)=g(u)]
Iff-And, 223
225 g(u)=g(u) => f(g(u))=u
Split, 224
226 f(g(u))=u => g(u)=g(u)
Split, 224
227 g(u)=g(u)
Reflex
228 f(g(u))=u
Detach, 225, 227
229 t=u
Substitute, 221, 228
As Required:
230 g(t)=g(u) => t=u
4 Conclusion, 210
As Required:
231 ALL(c):ALL(d):[c e y & d e y => [g(c)=g(d) => c=d]]
4 Conclusion, 207
As Required:
232 Injection(g,y,x)
Detach, 206, 231
Apply definition of Surjection
233 ALL(a):ALL(b):[Surjection(g,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & g(d)=c]]]
U Spec, 2
234 ALL(b):[Surjection(g,y,b) <=> ALL(c):[c e b => EXIST(d):[d e y & g(d)=c]]]
U Spec, 233
235 Surjection(g,y,x) <=> ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
U Spec, 234
236 [Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]]
& [ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]] => Surjection(g,y,x)]
Iff-And, 235
237 Surjection(g,y,x) => ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
Split, 236
Sufficient: Surjection(g,y,x)
238 ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]] => Surjection(g,y,x)
Split, 236
Prove: ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
Suppose...
239 t e x
Premise
240 t e x => f(t) e y
U Spec, 7
241 f(t) e y
Detach, 240, 239
Apply previous result
242 ALL(b):[t e x & b e y => [g(b)=t <=> f(t)=b]]
U Spec, 193
243 t e x & f(t) e y => [g(f(t))=t <=> f(t)=f(t)]
U Spec, 242
244 t e x & f(t) e y
Join, 239, 241
245 g(f(t))=t <=> f(t)=f(t)
Detach, 243, 244
246 [g(f(t))=t => f(t)=f(t)] & [f(t)=f(t) => g(f(t))=t]
Iff-And, 245
247 g(f(t))=t => f(t)=f(t)
Split, 246
248 f(t)=f(t) => g(f(t))=t
Split, 246
249 f(t)=f(t)
Reflex
250 g(f(t))=t
Detach, 248, 249
251 f(t) e y & g(f(t))=t
Join, 241, 250
252 EXIST(d):[d e y & g(d)=t]
E Gen, 251
As Required:
253 ALL(c):[c e x => EXIST(d):[d e y & g(d)=c]]
4 Conclusion, 239
254 Surjection(g,y,x)
Detach, 238, 253
255 Injection(g,y,x) & Surjection(g,y,x)
Join, 232, 254
256 Bijection(g,y,x)
Detach, 200, 255
257 ALL(a):[a e y => g(a) e x]
& ALL(a):ALL(b):[a e x & b e y => [g(b)=a <=> f(a)=b]]
Join, 144, 193
258 ALL(a):[a e y => g(a) e x]
& ALL(a):ALL(b):[a e x & b e y => [g(b)=a <=> f(a)=b]]
& Bijection(g,y,x)
Join, 257, 256
259 ALL(c):[c e y => g(c) e x]
& ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]
Join, 145, 194
260 ALL(c):[c e y => g(c) e x]
& ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]
& Bijection(g,y,x)
Join, 259, 256
As Required:
261 Bijection(f,x,y)
=> EXIST(g):[ALL(c):[c e y => g(c) e x]
& ALL(c):ALL(d):[c e x & d e y => [g(d)=c <=> f(c)=d]]
& Bijection(g,y,x)]
4 Conclusion, 8
As Required:
262 ALL(a):ALL(b):ALL(f):[Set(a) & Set(b) & ALL(c):[c e a => f(c) e b]
=> [Bijection(f,a,b)
=> EXIST(g):[ALL(c):[c e b => g(c) e a]
& ALL(c):ALL(d):[c e a & d e b => [g(d)=c <=> f(c)=d]]
& Bijection(g,b,a)]]]
4 Conclusion, 4