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