INTRODUCTION
************
From Richard Dedekind, a set X
is said to be infinite if and only if there exists a bijection mapping X to a
proper subset of X.
Equivalently, a set X is said
to be infinite if and only if there exists an injective but non-surjective
function mapping X to itself.
Here we prove this equivalency.
This formal proof was written
and machine-verified with the aid of the author’s DC Proof 2.0 freeware
available at http://www.dcproof.com
Dan Christensen
2021-6-5
THEOREM
*******
Let x be a set. Then we have:
There exists a bijection
mapping x to a proper subset y of x
EXIST(f):EXIST(y):[Set(y)
& ALL(a):[a e y => a e x]
& EXIST(a):[a
e x & ~a e y]
& ALL(a):[a e x => f(a) e y]
& ALL(a):ALL(b):[a
e x & b e x =>
[f(a)=f(b) => a=b]]
& ALL(a):[a e y => EXIST(b):[b e x &
f(b)=a]]]
If and only if there exists an
injective but non-surjective function mapping x to x
EXIST(f):[ALL(a):[a
e x => f(a) e x]
& [ALL(a):ALL(b):[a
e x & b e x =>
[f(a)=f(b) => a=b]]
& EXIST(a):[a
e x & ALL(b):[b e x =>
~f(b)=a]]]]
OUTLINE
*******
Let x be a set.
'=>'
Suppose we have function f: x -->
y where y is a proper subset of x, and f is both injective and surjective (a
bijection).
Construct function g: x -->
x where g(x)=f(x). Prove g is injective and not
surjective.
'<='
Suppose we have function f: x -->
x where f is injective and not surjective.
Construct function g: x -->
y where y is the range of f and g(x)=f(x). Prove g is
injective and surjective (a bijection).
PROOF
*****
Suppose...
1 Set(x)
Premise
'=>'
Suppose...
2 EXIST(f):EXIST(y):[Set(y)
& ALL(a):[a e y => a e x] &
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
Premise
3 EXIST(y):[Set(y) & ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
E Spec, 2
4 Set(y) & ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]
E Spec, 3
y is a proper subset of x
5 Set(y)
Split, 4
6 ALL(a):[a e y => a e x]
Split, 4
7 EXIST(a):[a e x & ~a e y]
Split, 4
f is a bijection mapping x to y
8 ALL(a):[a e x => f(a) e y]
Split, 4
9 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Split, 4
10 ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]
Split, 4
Construct function g: x -->x such that g(x)=f(x)
Apply Cartesian Product
Axiom
11 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
12 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, 11
13 Set(x) & Set(x) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]
U Spec, 12
14 Set(x) & Set(x)
Join, 1, 1
15 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e x]]
Detach, 13, 14
16 Set'(x2) & ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]
E Spec, 15
Define: x2
17 Set'(x2)
Split, 16
18 ALL(c1):ALL(c2):[(c1,c2) e x2 <=> c1 e x & c2 e x]
Split, 16
19 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x2 & b=f(a)]]
Subset, 17
20 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & b=f(a)]
E Spec, 19
Define: g
21 Set'(g)
Split, 20
22 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e x2 & b=f(a)]
Split, 20
23 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
24 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, 23
25 ALL(cod):[Set'(g) & Set(x) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e cod]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e cod & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e cod => [g(a1)=b <=> (a1,b) e g]]]]
U Spec, 24
26 Set'(g) & Set(x) & Set(x)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e x => [g(a1)=b <=> (a1,b) e g]]]
U Spec, 25
27 Set'(g) & Set(x)
Join, 21, 1
28 Set'(g) & Set(x) & Set(x)
Join, 27, 1
Sufficient: For functionality of g
29 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e x => [g(a1)=b <=> (a1,b) e g]]
Detach, 26, 28
Prove: ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
Suppose...
30 (t,u) e g
Premise
31 ALL(b):[(t,b) e g <=> (t,b) e x2 & b=f(t)]
U Spec, 22
32 (t,u) e g <=> (t,u) e x2 & u=f(t)
U Spec, 31
33 [(t,u) e g => (t,u) e x2 & u=f(t)]
&
[(t,u) e x2 & u=f(t) => (t,u) e g]
Iff-And, 32
34 (t,u) e g => (t,u) e x2 & u=f(t)
Split, 33
35 (t,u) e x2 & u=f(t)
Detach, 34, 30
36 (t,u) e x2
Split, 35
37 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]
U Spec, 18
38 (t,u) e x2 <=> t e x & u e x
U Spec, 37
39 [(t,u) e x2 => t e x & u e x]
&
[t e x & u e x => (t,u) e x2]
Iff-And, 38
40 (t,u) e x2 => t e x & u e x
Split, 39
41 t e x & u e x
Detach, 40, 36
Part 1
42 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
4 Conclusion, 30
Prove: ALL(a1):[a1 e x => EXIST(b):[b e x &
(a1,b) e g]]
Suppose...
43 t e x
Premise
44 t e x => f(t) e y
U Spec, 8
45 f(t) e y
Detach, 44, 43
46 ALL(b):[(t,b) e g <=> (t,b) e x2 & b=f(t)]
U Spec, 22
47 (t,f(t)) e g <=> (t,f(t)) e x2 & f(t)=f(t)
U Spec, 46, 45
48 [(t,f(t)) e g => (t,f(t)) e x2 & f(t)=f(t)]
&
[(t,f(t)) e x2 & f(t)=f(t) => (t,f(t)) e g]
Iff-And, 47
Sufficient: For (t,f(t))
e g
49 (t,f(t)) e x2 & f(t)=f(t) => (t,f(t)) e g
Split, 48
50 ALL(c2):[(t,c2) e x2 <=> t e x & c2 e x]
U Spec, 18
51 (t,f(t)) e x2 <=> t e x & f(t) e x
U Spec, 50, 45
52 [(t,f(t)) e x2 => t e x & f(t) e x]
&
[t e x & f(t) e x => (t,f(t)) e x2]
Iff-And, 51
53 (t,f(t)) e x2 => t e x & f(t) e x
Split, 52
Sufficient: For (t,f(t))
e x2
54 t e x & f(t) e x => (t,f(t)) e x2
Split, 52
55 f(t) e y => f(t) e x
U Spec, 6, 45
56 f(t) e x
Detach, 55, 45
57 t e x & f(t) e x
Join, 43, 56
58 (t,f(t)) e x2
Detach, 54, 57
59 f(t)=f(t)
Reflex, 56
60 (t,f(t)) e x2 & f(t)=f(t)
Join, 58, 59
61 (t,f(t)) e g
Detach, 49, 60
62 f(t) e x & (t,f(t)) e g
Join, 56, 61
63 EXIST(b):[b e x & (t,b) e g]
E Gen, 62
Part 2
64 ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e g]]
4 Conclusion, 43
Prove: ALL(a1):ALL(b1):ALL(b2):[a1
e x & b1 e x & b2 e x
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
Suppose...
65 t e x & u1 e x & u2 e x
Premise
66 t e x
Split, 65
67 u1 e x
Split, 65
68 u2 e x
Split, 65
Suppose...
69 (t,u1) e g & (t,u2) e g
Premise
70 (t,u1) e g
Split, 69
71 (t,u2) e g
Split, 69
72 ALL(b):[(t,b) e g <=> (t,b) e x2 & b=f(t)]
U Spec, 22
73 (t,u1) e g <=> (t,u1) e x2 & u1=f(t)
U Spec, 72
74 [(t,u1) e g => (t,u1) e x2 & u1=f(t)]
&
[(t,u1) e x2 & u1=f(t) => (t,u1) e g]
Iff-And, 73
75 (t,u1) e g => (t,u1) e x2 & u1=f(t)
Split, 74
76 (t,u1) e x2 & u1=f(t)
Detach, 75, 70
77 (t,u1) e x2
Split, 76
78 u1=f(t)
Split, 76
79 (t,u2) e g <=> (t,u2) e x2 & u2=f(t)
U Spec, 72
80 [(t,u2) e g => (t,u2) e x2 & u2=f(t)]
&
[(t,u2) e x2 & u2=f(t) => (t,u2) e g]
Iff-And, 79
81 (t,u2) e g => (t,u2) e x2 & u2=f(t)
Split, 80
82 (t,u2) e x2 & u2=f(t)
Detach, 81, 71
83 u2=f(t)
Split, 82
84 u1=u2
Substitute, 83,
78
As Required:
85 (t,u1) e g & (t,u2) e g => u1=u2
4 Conclusion, 69
Part 3
86 ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
4 Conclusion, 65
87 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e g]]
Join, 42, 64
88 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e x]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e x & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e x & b2 e x
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
Join, 87, 86
g is a function
89 ALL(a1):ALL(b):[a1 e x & b e x => [g(a1)=b <=> (a1,b) e g]]
Detach, 29, 88
Prove: ALL(a):[a e x => g(a) e x]
Suppose...
90 t e x
Premise
91 t e x => EXIST(b):[b e x & (t,b) e g]
U Spec, 64
92 EXIST(b):[b e x & (t,b) e g]
Detach, 91, 90
93 u e x & (t,u) e g
E Spec, 92
94 u e x
Split, 93
95 (t,u) e g
Split, 93
96 ALL(b):[t e x & b e x => [g(t)=b <=> (t,b) e g]]
U Spec, 89
97 t e x & u e x => [g(t)=u <=> (t,u) e g]
U Spec, 96
98 t e x & u e x
Join, 90, 94
99 g(t)=u <=> (t,u) e g
Detach, 97, 98
100 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 99
101 (t,u) e g => g(t)=u
Split, 100
102 g(t)=u
Detach, 101, 95
103 g(t) e x
Substitute, 102,
94
As Required:
104 ALL(a):[a e x => g(a) e x]
4 Conclusion, 90
Prove: ALL(a):[a e x => g(a)=f(a)]
Suppose...
105 t e x
Premise
106 t e x => EXIST(b):[b e x & (t,b) e g]
U Spec, 64
107 EXIST(b):[b e x & (t,b) e g]
Detach, 106, 105
108 u e x & (t,u) e g
E Spec, 107
109 u e x
Split, 108
110 (t,u) e g
Split, 108
111 ALL(b):[(t,b) e g <=> (t,b) e x2 & b=f(t)]
U Spec, 22
112 (t,u) e g <=> (t,u) e x2 & u=f(t)
U Spec, 111
113 [(t,u) e g => (t,u) e x2 & u=f(t)]
&
[(t,u) e x2 & u=f(t) => (t,u) e g]
Iff-And, 112
114 (t,u) e g => (t,u) e x2 & u=f(t)
Split, 113
115 (t,u) e x2 & u=f(t)
Detach, 114, 110
116 (t,u) e x2
Split, 115
117 u=f(t)
Split, 115
118 ALL(b):[t e x & b e x => [g(t)=b <=> (t,b) e g]]
U Spec, 89
119 t e x & u e x => [g(t)=u <=> (t,u) e g]
U Spec, 118
120 t e x & u e x
Join, 105, 109
121 g(t)=u <=> (t,u) e g
Detach, 119, 120
122 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 121
123 (t,u) e g => g(t)=u
Split, 122
124 g(t)=u
Detach, 123, 110
125 g(t)=f(t)
Substitute, 117,
124
As Required:
126 ALL(a):[a e x => g(a)=f(a)]
4 Conclusion, 105
Prove: g is injective
Suppose...
127 t e x & u e x
Premise
128 t e x
Split, 127
129 u e x
Split, 127
Suppose...
130 g(t)=g(u)
Premise
131 t e x => g(t)=f(t)
U Spec, 126
132 g(t)=f(t)
Detach, 131, 128
133 u e x => g(u)=f(u)
U Spec, 126
134 g(u)=f(u)
Detach, 133, 129
135 ALL(b):[t e x & b e x => [f(t)=f(b) => t=b]]
U Spec, 9
136 t e x & u e x => [f(t)=f(u) => t=u]
U Spec, 135
137 f(t)=f(u) => t=u
Detach, 136, 127
138 f(t)=g(u)
Substitute, 132,
130
139 f(t)=f(u)
Substitute, 134,
138
140 t=u
Detach, 137, 139
141 g(t)=g(u) => t=u
4 Conclusion, 130
g is injective
As Required:
142 ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
4 Conclusion, 127
143 z e x & ~z e y
E Spec, 7
Define: z
144 z e x
Split, 143
145 ~z e y
Split, 143
Prove: ALL(b):[b e x => ~g(b)=z]
Suppose...
146 t e x
Premise
Suppose to the contrary...
147 g(t)=z
Premise
148 t e x => g(t)=f(t)
U Spec, 126
149 g(t)=f(t)
Detach, 148, 146
150 f(t)=z
Substitute, 149,
147
151 t e x => f(t) e y
U Spec, 8
152 f(t) e y
Detach, 151, 146
153 z e y
Substitute, 150,
152
154 z e y & ~z e y
Join, 153, 145
As Required:
155 ~g(t)=z
4 Conclusion, 147
As Required:
156 ALL(b):[b e x => ~g(b)=z]
4 Conclusion, 146
157 z e x & ALL(b):[b e x => ~g(b)=z]
Join, 144, 156
g is not surjective
158 EXIST(a):[a e x & ALL(b):[b e x => ~g(b)=a]]
E Gen, 157
159 ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~g(b)=a]]
Join, 142, 158
160 ALL(a):[a e x => g(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~g(b)=a]]]
Join, 104, 159
161 EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
E Gen, 160
As Required:
162 EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
=>
EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
4 Conclusion, 2
Prove the converse
'<='
Suppose...
163 EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
Premise
164 ALL(a):[a e x => f(a) e x]
& [ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]
E Spec, 163
165 ALL(a):[a e x => f(a) e x]
Split, 164
166 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Split, 164
f is injective
167 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Split, 166
f is not surjective
168 EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Split, 166
169 z e x & ALL(b):[b e x => ~f(b)=z]
E Spec, 168
Define: z
170 z e x
Split, 169
171 ALL(b):[b e x => ~f(b)=z]
Split, 169
Construct function g: x --> y,
where y is the range of f
Apply Subset Axiom
172 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x &
EXIST(b):[b e x & a=f(b)]]]
Subset, 1
173 Set(y) & ALL(a):[a e y <=> a e x & EXIST(b):[b e x & a=f(b)]]
E Spec, 172
Define: y f(x)
174 Set(y)
Split, 173
175 ALL(a):[a e y <=> a e x & EXIST(b):[b e x & a=f(b)]]
Split, 173
176 z e y <=> z e x & EXIST(b):[b e x & z=f(b)]
U Spec, 175
177 [z e y => z e x & EXIST(b):[b e x & z=f(b)]]
&
[z e x & EXIST(b):[b e x & z=f(b)] => z e y]
Iff-And, 176
178 z e y => z e x & EXIST(b):[b e x & z=f(b)]
Split, 177
179 ~[z e x &
EXIST(b):[b e x & z=f(b)]] => ~z e y
Contra, 178
180 ~~[~z e x | ~EXIST(b):[b e x & z=f(b)]] => ~z e y
DeMorgan, 179
181 ~z e x | ~EXIST(b):[b e x & z=f(b)] => ~z e y
Rem DNeg, 180
182 ~z e x | ~~ALL(b):~[b e x & z=f(b)] => ~z e y
Quant, 181
183 ~z e x | ALL(b):~[b e x & z=f(b)] => ~z e y
Rem DNeg, 182
184 ~z e x | ALL(b):~~[b e x => ~z=f(b)] => ~z e y
Imply-And, 183
185 ~z e x | ALL(b):[b e x => ~z=f(b)] => ~z e y
Rem DNeg, 184
186 ~z e x | ALL(b):[b e x => ~f(b)=z] => ~z e y
Sym, 185
187 ~z e x | ALL(b):[b e x => ~f(b)=z]
Arb Or, 171
As Required:
188 ~z e y
Detach, 186, 187
Suppose...
189 t e y
Premise
190 t e y <=> t e x & EXIST(b):[b e x & t=f(b)]
U Spec, 175
191 [t e y => t e x & EXIST(b):[b e x & t=f(b)]]
&
[t e x & EXIST(b):[b e x & t=f(b)] => t e y]
Iff-And, 190
192 t e y => t e x & EXIST(b):[b e x & t=f(b)]
Split, 191
193 t e x & EXIST(b):[b e x & t=f(b)]
Detach, 192, 189
194 t e x
Split, 193
As Required:
195 ALL(a):[a e y => a e x]
4 Conclusion, 189
196 z e x & ~z e y
Join, 170, 188
As Required:
197 EXIST(a):[a e x & ~a e y]
E Gen, 196
198 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
199 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, 198
200 Set(x) & Set(y) => EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
U Spec, 199
201 Set(x) & Set(y)
Join, 1, 174
202 EXIST(b):[Set'(b) &
ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x & c2 e y]]
Detach, 200, 201
203 Set'(xy) & ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
E Spec, 202
Define: xy
204 Set'(xy)
Split, 203
205 ALL(c1):ALL(c2):[(c1,c2) e xy <=> c1 e x & c2 e y]
Split, 203
206 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e xy & b=f(a)]]
Subset, 204
207 Set'(g) & ALL(a):ALL(b):[(a,b) e g <=> (a,b) e xy & b=f(a)]
E Spec, 206
Define: g
208 Set'(g)
Split, 207
209 ALL(a):ALL(b):[(a,b) e g <=> (a,b) e xy & b=f(a)]
Split, 207
210 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
211 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, 210
212 ALL(cod):[Set'(g) & Set(x) & Set(cod)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e cod]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e cod & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e cod & b2 e cod
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e cod => [g(a1)=b <=> (a1,b) e g]]]]
U Spec, 211
213 Set'(g) & Set(x) & Set(y)
=>
[ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e y => [g(a1)=b <=> (a1,b) e g]]]
U Spec, 212
214 Set'(g) & Set(x)
Join, 208, 1
215 Set'(g) & Set(x) & Set(y)
Join, 214, 174
Sufficient: For functionality of g
216 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
=>
ALL(a1):ALL(b):[a1 e x & b e y => [g(a1)=b <=> (a1,b) e g]]
Detach, 213, 215
Prove: ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
Suppose...
217 (t,u) e g
Premise
218 ALL(b):[(t,b) e g <=> (t,b) e xy & b=f(t)]
U Spec, 209
219 (t,u) e g <=> (t,u) e xy & u=f(t)
U Spec, 218
220 [(t,u) e g => (t,u) e xy & u=f(t)]
&
[(t,u) e xy & u=f(t) => (t,u) e g]
Iff-And, 219
221 (t,u) e g => (t,u) e xy & u=f(t)
Split, 220
222 (t,u) e xy & u=f(t)
Detach, 221, 217
223 (t,u) e xy
Split, 222
224 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 205
225 (t,u) e xy <=> t e x & u e y
U Spec, 224
226 [(t,u) e xy => t e x & u e y]
&
[t e x & u e y => (t,u) e xy]
Iff-And, 225
227 (t,u) e xy => t e x & u e y
Split, 226
228 t e x & u e y
Detach, 227, 223
Part 1
229 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
4 Conclusion, 217
Prove: ALL(a1):[a1 e x => EXIST(b):[b e y &
(a1,b) e g]]
Suppose...
230 t e x
Premise
231 t e x => f(t) e x
U Spec, 165
232 f(t) e x
Detach, 231, 230
233 ALL(b):[(t,b) e g <=> (t,b) e xy & b=f(t)]
U Spec, 209
234 (t,f(t)) e g <=> (t,f(t)) e xy & f(t)=f(t)
U Spec, 233, 232
235 [(t,f(t)) e g => (t,f(t)) e xy & f(t)=f(t)]
&
[(t,f(t)) e xy & f(t)=f(t) => (t,f(t)) e g]
Iff-And, 234
Sufficient: For (t,f(t))
e g
236 (t,f(t)) e xy & f(t)=f(t) => (t,f(t)) e g
Split, 235
237 ALL(c2):[(t,c2) e xy <=> t e x & c2 e y]
U Spec, 205
238 (t,f(t)) e xy <=> t e x & f(t) e y
U Spec, 237, 232
239 [(t,f(t)) e xy => t e x & f(t) e y]
&
[t e x & f(t) e y => (t,f(t)) e xy]
Iff-And, 238
240 (t,f(t)) e xy => t e x & f(t) e y
Split, 239
Sufficient: For (t,f(t))
e xy
241 t e x & f(t) e y => (t,f(t)) e xy
Split, 239
242 f(t) e y <=> f(t) e x & EXIST(b):[b e x & f(t)=f(b)]
U Spec, 175, 232
243 [f(t) e y => f(t) e x &
EXIST(b):[b e x & f(t)=f(b)]]
&
[f(t) e x & EXIST(b):[b e x & f(t)=f(b)] => f(t) e y]
Iff-And, 242
Sufficient:
244 f(t) e x &
EXIST(b):[b e x & f(t)=f(b)] => f(t) e y
Split, 243
245 f(t)=f(t)
Reflex, 232
246 t e x & f(t)=f(t)
Join, 230, 245
247 EXIST(b):[b e x & f(t)=f(b)]
E Gen, 246
248 f(t) e x &
EXIST(b):[b e x & f(t)=f(b)]
Join, 232, 247
249 f(t) e y
Detach, 244, 248
250 t e x & f(t) e y
Join, 230, 249
251 (t,f(t)) e xy
Detach, 241, 250
252 (t,f(t)) e xy & f(t)=f(t)
Join, 251, 245
253 (t,f(t)) e g
Detach, 236, 252
254 f(t) e y & (t,f(t)) e g
Join, 249, 253
255 EXIST(b):[b e y & (t,b) e g]
E Gen, 254
Part 2
256 ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
4 Conclusion, 230
Prove: ALL(a1):ALL(b1):ALL(b2):[a1
e x & b1 e y & b2 e y
=> [(a1,b1) e g & (a1,b2) e g => b1=b2]]
Suppose...
257 t e x & u1 e y & u2 e y
Premise
258 t e x
Split, 257
259 u1 e y
Split, 257
260 u2 e y
Split, 257
261 (t,u1) e g & (t,u2) e g
Premise
262 (t,u1) e g
Split, 261
263 (t,u2) e g
Split, 261
264 ALL(b):[(t,b) e g <=> (t,b) e xy & b=f(t)]
U Spec, 209
265 (t,u1) e g <=> (t,u1) e xy & u1=f(t)
U Spec, 264
266 [(t,u1) e g => (t,u1) e xy & u1=f(t)]
&
[(t,u1) e xy & u1=f(t) => (t,u1) e g]
Iff-And, 265
267 (t,u1) e g => (t,u1) e xy & u1=f(t)
Split, 266
268 (t,u1) e xy & u1=f(t) => (t,u1) e g
Split, 266
269 (t,u1) e xy & u1=f(t)
Detach, 267, 262
270 u1=f(t)
Split, 269
271 (t,u2) e g <=> (t,u2) e xy & u2=f(t)
U Spec, 264
272 [(t,u2) e g => (t,u2) e xy & u2=f(t)]
&
[(t,u2) e xy & u2=f(t) => (t,u2) e g]
Iff-And, 271
273 (t,u2) e g => (t,u2) e xy & u2=f(t)
Split, 272
274 (t,u2) e xy & u2=f(t)
Detach, 273, 263
275 u2=f(t)
Split, 274
276 u1=u2
Substitute, 275,
270
277 (t,u1) e g & (t,u2) e g => u1=u2
4 Conclusion, 261
Part 3
278 ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
4 Conclusion, 257
279 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
Join, 229, 256
280 ALL(a1):ALL(b):[(a1,b) e g => a1 e x & b e y]
&
ALL(a1):[a1 e x =>
EXIST(b):[b e y & (a1,b) e g]]
&
ALL(a1):ALL(b1):ALL(b2):[a1 e x & b1 e y & b2 e y
=>
[(a1,b1) e g & (a1,b2) e g => b1=b2]]
Join, 279, 278
g is a function mapping x to y
281 ALL(a1):ALL(b):[a1 e x & b e y => [g(a1)=b <=> (a1,b) e g]]
Detach, 216, 280
Suppose...
282 t e x
Premise
283 t e x => EXIST(b):[b e y & (t,b) e g]
U Spec, 256
284 EXIST(b):[b e y & (t,b) e g]
Detach, 283, 282
285 u e y & (t,u) e g
E Spec, 284
286 u e y
Split, 285
287 (t,u) e g
Split, 285
288 ALL(b):[t e x & b e y => [g(t)=b <=> (t,b) e g]]
U Spec, 281
289 t e x & u e y => [g(t)=u <=> (t,u) e g]
U Spec, 288
290 t e x & u e y
Join, 282, 286
291 g(t)=u <=> (t,u) e g
Detach, 289, 290
292 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 291
293 (t,u) e g => g(t)=u
Split, 292
294 g(t)=u
Detach, 293, 287
295 g(t) e y
Substitute, 294,
286
As Required:
296 ALL(a):[a e x => g(a) e y]
4 Conclusion, 282
297 t e x
Premise
298 t e x => EXIST(b):[b e y & (t,b) e g]
U Spec, 256
299 EXIST(b):[b e y & (t,b) e g]
Detach, 298, 297
300 u e y & (t,u) e g
E Spec, 299
301 u e y
Split, 300
302 (t,u) e g
Split, 300
303 ALL(b):[(t,b) e g <=> (t,b) e xy & b=f(t)]
U Spec, 209
304 (t,u) e g <=> (t,u) e xy & u=f(t)
U Spec, 303
305 [(t,u) e g => (t,u) e xy & u=f(t)]
&
[(t,u) e xy & u=f(t) => (t,u) e g]
Iff-And, 304
306 (t,u) e g => (t,u) e xy & u=f(t)
Split, 305
307 (t,u) e xy & u=f(t)
Detach, 306, 302
308 (t,u) e xy
Split, 307
309 u=f(t)
Split, 307
310 ALL(b):[t e x & b e y => [g(t)=b <=> (t,b) e g]]
U Spec, 281
311 t e x & u e y => [g(t)=u <=> (t,u) e g]
U Spec, 310
312 t e x & u e y
Join, 297, 301
313 g(t)=u <=> (t,u) e g
Detach, 311, 312
314 [g(t)=u => (t,u) e g] & [(t,u) e g => g(t)=u]
Iff-And, 313
315 (t,u) e g => g(t)=u
Split, 314
316 g(t)=u
Detach, 315, 302
317 g(t)=f(t)
Substitute, 309,
316
As Required:
318 ALL(a):[a e x => g(a)=f(a)]
4 Conclusion, 297
Suppose...
319 t e x & u e x
Premise
320 t e x
Split, 319
321 u e x
Split, 319
Suppose...
322 g(t)=g(u)
Premise
323 t e x => g(t)=f(t)
U Spec, 318
324 g(t)=f(t)
Detach, 323, 320
325 u e x => g(u)=f(u)
U Spec, 318
326 g(u)=f(u)
Detach, 325, 321
327 f(t)=g(u)
Substitute, 324,
322
328 f(t)=f(u)
Substitute, 326,
327
329 ALL(b):[t e x & b e x => [f(t)=f(b) => t=b]]
U Spec, 167
330 t e x & u e x => [f(t)=f(u) => t=u]
U Spec, 329
331 f(t)=f(u) => t=u
Detach, 330, 319
332 t=u
Detach, 331, 328
333 g(t)=g(u) => t=u
4 Conclusion, 322
g is injective
334 ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
4 Conclusion, 319
Suppose...
335 t e y
Premise
336 t e y <=> t e x & EXIST(b):[b e x & t=f(b)]
U Spec, 175
337 [t e y => t e x & EXIST(b):[b e x & t=f(b)]]
&
[t e x & EXIST(b):[b e x & t=f(b)] => t e y]
Iff-And, 336
338 t e y => t e x & EXIST(b):[b e x & t=f(b)]
Split, 337
339 t e x & EXIST(b):[b e x & t=f(b)]
Detach, 338, 335
340 t e x
Split, 339
341 EXIST(b):[b e x & t=f(b)]
Split, 339
342 v e x & t=f(v)
E Spec, 341
343 v e x
Split, 342
344 t=f(v)
Split, 342
345 v e x => g(v)=f(v)
U Spec, 318
346 g(v)=f(v)
Detach, 345, 343
347 v e x & t=g(v)
Substitute, 346,
342
348 v e x & g(v)=t
Sym, 347
349 EXIST(b):[b e x & g(b)=t]
E Gen, 348
g is surjective
350 ALL(a):[a e y =>
EXIST(b):[b e x & g(b)=a]]
4 Conclusion, 335
351 Set(y) & ALL(a):[a e y => a e x]
Join, 174, 195
352 Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
Join, 351, 197
353 Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => g(a) e y]
Join, 352, 296
354 Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => g(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
Join, 353, 334
355 Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => g(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & g(b)=a]]
Join, 354, 350
356 EXIST(y):[Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => g(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [g(a)=g(b) => a=b]]
&
ALL(a):[a e y => EXIST(b):[b e x & g(b)=a]]]
E Gen, 355
357 EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
E Gen, 356
358 EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
=>
EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
4 Conclusion, 163
359 [EXIST(f):EXIST(y):[Set(y) &
ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
=>
EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]]
&
[EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
=>
EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x]
&
EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]]
Join, 162, 358
360 EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y =>
EXIST(b):[b e x & f(b)=a]]]
<=>
EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]]]
Iff-And, 359
361 ALL(x):[Set(x)
=>
[EXIST(f):EXIST(y):[Set(y) & ALL(a):[a e y => a e x] & EXIST(a):[a e x & ~a e y]
&
ALL(a):[a e x => f(a) e y]
&
ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
ALL(a):[a e y => EXIST(b):[b e x & f(b)=a]]]
<=>
EXIST(f):[ALL(a):[a e x => f(a) e x]
&
[ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
&
EXIST(a):[a e x &
ALL(b):[b e x => ~f(b)=a]]]]]]
4 Conclusion, 1