Theorem
*******
(Commentary in blue text.)
If x is a finite set and f is an injective (1-1) function on x, then f is surjective (onto).
Formally:
ALL(x):ALL(f):[Set(x)
& ~Infinite(x)
& 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]]
=> ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]
Outline of Proof
****************
Suppose that f is an injective (1-1) function defined on set x. Using proof by contrapositive, suppose that
f is not surjective (onto) and prove that x must be infinite.
Let set x' be the image of set x under f. Construct the function f' being the inverse of f on x'. Prove that
f' is both injective (1-1) and surjective (onto), that x must therefore be infinite.
From the contrapostive, we have: If x is finite, then f must be surjective (onto).
This proof written with the aid of the author's DC Proof 2.0 software available at http://www.dcproof.com
Define: Infinite
****************
Set s is infinite iff there exists a proper subset s' of s and function f such that f is bijection
mapping s' to s.
1 ALL(s):[Set(s) => [Infinite(s)
<=> EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e s]
& EXIST(a):[a e s & ~a e s']
& ALL(a):[a e s' => f(a) e s]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e s => EXIST(b):[b e s' & f(b)=a]]]]]
Axiom
Prove: ALL(x):[Set(x)
=> ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]]
Suppose...
2 Set(x)
Premise
Apply definition of infinite
3 Set(x) => [Infinite(x)
<=> EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]]]
U Spec, 1
4 Infinite(x)
<=> EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]]
Detach, 3, 2
5 [Infinite(x) => EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]]]
& [EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]] => Infinite(x)]
Iff-And, 4
6 Infinite(x) => EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]]
Split, 5
Sufficient: For Infinite(x)
7 EXIST(s'):EXIST(f):[Set(s')
& ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]] => Infinite(x)
Split, 5
Prove: ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]
Let f be an injective (1-1) function on x
8 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]]
Premise
9 ALL(a):[a e x => f(a) e x]
Split, 8
10 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Split, 8
Prove: ~ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
=> Infinite(x)
Suppose f is not surjective
11 ~ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
Premise
12 ~~EXIST(a):~[a e x => EXIST(b):[b e x & f(b)=a]]
Quant, 11
13 EXIST(a):~[a e x => EXIST(b):[b e x & f(b)=a]]
Rem DNeg, 12
14 EXIST(a):~~[a e x & ~EXIST(b):[b e x & f(b)=a]]
Imply-And, 13
15 EXIST(a):[a e x & ~EXIST(b):[b e x & f(b)=a]]
Rem DNeg, 14
16 EXIST(a):[a e x & ~~ALL(b):~[b e x & f(b)=a]]
Quant, 15
17 EXIST(a):[a e x & ALL(b):~[b e x & f(b)=a]]
Rem DNeg, 16
18 EXIST(a):[a e x & ALL(b):~~[b e x => ~f(b)=a]]
Imply-And, 17
Alternatively...
19 EXIST(a):[a e x & ALL(b):[b e x => ~f(b)=a]]
Rem DNeg, 18
20 y e x & ALL(b):[b e x => ~f(b)=y]
E Spec, 19
Let y in x have no pre-image under f
21 y e x
Split, 20
22 ALL(b):[b e x => ~f(b)=y]
Split, 20
Construct the set x'=f(x)
Apply Subset Axiom
23 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e x & EXIST(b):[b e x & f(b)=a]]]
Subset, 2
24 Set(x') & ALL(a):[a e x' <=> a e x & EXIST(b):[b e x & f(b)=a]]
E Spec, 23
Define: x'
**********
Let x' be the image of set x under f
25 Set(x')
Split, 24
Every element of x' has a pre-image under f.
26 ALL(a):[a e x' <=> a e x & EXIST(b):[b e x & f(b)=a]]
Split, 24
Prove: x' is a subset of x
Suppose...
27 p e x'
Premise
Apply definition of x'
28 p e x' <=> p e x & EXIST(b):[b e x & f(b)=p]
U Spec, 26
29 [p e x' => p e x & EXIST(b):[b e x & f(b)=p]]
& [p e x & EXIST(b):[b e x & f(b)=p] => p e x']
Iff-And, 28
30 p e x' => p e x & EXIST(b):[b e x & f(b)=p]
Split, 29
31 p e x & EXIST(b):[b e x & f(b)=p] => p e x'
Split, 29
32 p e x & EXIST(b):[b e x & f(b)=p]
Detach, 30, 27
33 p e x
Split, 32
x' is a subset of x
As Required:
34 ALL(a):[a e x' => a e x]
4 Conclusion, 27
Prove: x' is a proper subset of x
Apply definition of x'
35 y e x' <=> y e x & EXIST(b):[b e x & f(b)=y]
U Spec, 26
36 [y e x' => y e x & EXIST(b):[b e x & f(b)=y]]
& [y e x & EXIST(b):[b e x & f(b)=y] => y e x']
Iff-And, 35
37 y e x' => y e x & EXIST(b):[b e x & f(b)=y]
Split, 36
38 y e x & EXIST(b):[b e x & f(b)=y] => y e x'
Split, 36
39 ~[y e x & EXIST(b):[b e x & f(b)=y]] => ~y e x'
Contra, 37
40 ~~[~y e x | ~EXIST(b):[b e x & f(b)=y]] => ~y e x'
DeMorgan, 39
41 ~y e x | ~EXIST(b):[b e x & f(b)=y] => ~y e x'
Rem DNeg, 40
42 ~y e x | ~~ALL(b):~[b e x & f(b)=y] => ~y e x'
Quant, 41
43 ~y e x | ALL(b):~[b e x & f(b)=y] => ~y e x'
Rem DNeg, 42
44 ~y e x | ALL(b):~~[b e x => ~f(b)=y] => ~y e x'
Imply-And, 43
45 ~y e x | ALL(b):[b e x => ~f(b)=y] => ~y e x'
Rem DNeg, 44
46 ~y e x | ALL(b):[b e x => ~f(b)=y]
Arb Or, 22
47 ~y e x'
Detach, 45, 46
48 y e x & ~y e x'
Join, 21, 47
x' is a proper subset of x
As Required:
49 EXIST(a):[a e x & ~a e x']
E Gen, 48
Construct Cartesian product of x' and x
Apply Cartesian Product Axiom
50 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
51 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, 50
52 Set(x') & Set(x) => EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x' & c2 e x]]
U Spec, 51
53 Set(x') & Set(x)
Join, 25, 2
54 EXIST(b):[Set'(b) & ALL(c1):ALL(c2):[(c1,c2) e b <=> c1 e x' & c2 e x]]
Detach, 52, 53
55 Set'(x'x) & ALL(c1):ALL(c2):[(c1,c2) e x'x <=> c1 e x' & c2 e x]
E Spec, 54
Define: x'x (Cartesian product of x' and x)
***********
56 Set'(x'x)
Split, 55
57 ALL(c1):ALL(c2):[(c1,c2) e x'x <=> c1 e x' & c2 e x]
Split, 55
Construct set of ordered pairs f'
Apply Subset Axiom
58 EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e x'x & f(b)=a]]
Subset, 56
59 Set'(f') & ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e x'x & f(b)=a]
E Spec, 58
Define: f' (the inverse of f on x')
60 Set'(f')
Split, 59
61 ALL(a):ALL(b):[(a,b) e f' <=> (a,b) e x'x & f(b)=a]
Split, 59
Prove: f' is a function
Axiom Function Axiom
62 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
63 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']]
U Spec, 62
64 ALL(b):[ALL(c):ALL(d):[(c,d) e f' => c e x' & d e b]
& ALL(c):[c e x' => 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']]
U Spec, 63
Sufficient: For functionality of f'
65 ALL(c):ALL(d):[(c,d) e f' => c e x' & d e x]
& ALL(c):[c e x' => EXIST(d):[d e x & (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']
U Spec, 64
Prove: ALL(c):ALL(d):[(c,d) e f' => c e x' & d e x]
Suppose...
66 (p,q) e f'
Premise
Apply definition of f'
67 ALL(b):[(p,b) e f' <=> (p,b) e x'x & f(b)=p]
U Spec, 61
68 (p,q) e f' <=> (p,q) e x'x & f(q)=p
U Spec, 67
69 [(p,q) e f' => (p,q) e x'x & f(q)=p]
& [(p,q) e x'x & f(q)=p => (p,q) e f']
Iff-And, 68
70 (p,q) e f' => (p,q) e x'x & f(q)=p
Split, 69
71 (p,q) e x'x & f(q)=p => (p,q) e f'
Split, 69
72 (p,q) e x'x & f(q)=p
Detach, 70, 66
73 (p,q) e x'x
Split, 72
74 f(q)=p
Split, 72
Apply definition of x'x
75 ALL(c2):[(p,c2) e x'x <=> p e x' & c2 e x]
U Spec, 57
76 (p,q) e x'x <=> p e x' & q e x
U Spec, 75
77 [(p,q) e x'x => p e x' & q e x]
& [p e x' & q e x => (p,q) e x'x]
Iff-And, 76
78 (p,q) e x'x => p e x' & q e x
Split, 77
79 p e x' & q e x => (p,q) e x'x
Split, 77
80 p e x' & q e x
Detach, 78, 73
As Required:
81 ALL(c):ALL(d):[(c,d) e f' => c e x' & d e x]
4 Conclusion, 66
Prove: ALL(c):[c e x' => EXIST(d):[d e x & (c,d) e f']]
Suppose...
82 p e x'
Premise
Apply definition of x'
83 p e x' <=> p e x & EXIST(b):[b e x & f(b)=p]
U Spec, 26
84 [p e x' => p e x & EXIST(b):[b e x & f(b)=p]]
& [p e x & EXIST(b):[b e x & f(b)=p] => p e x']
Iff-And, 83
85 p e x' => p e x & EXIST(b):[b e x & f(b)=p]
Split, 84
86 p e x & EXIST(b):[b e x & f(b)=p] => p e x'
Split, 84
87 p e x & EXIST(b):[b e x & f(b)=p]
Detach, 85, 82
88 p e x
Split, 87
89 EXIST(b):[b e x & f(b)=p]
Split, 87
90 q e x & f(q)=p
E Spec, 89
91 q e x
Split, 90
92 f(q)=p
Split, 90
Apply definition of f'
93 ALL(b):[(p,b) e f' <=> (p,b) e x'x & f(b)=p]
U Spec, 61
94 (p,q) e f' <=> (p,q) e x'x & f(q)=p
U Spec, 93
95 [(p,q) e f' => (p,q) e x'x & f(q)=p]
& [(p,q) e x'x & f(q)=p => (p,q) e f']
Iff-And, 94
96 (p,q) e f' => (p,q) e x'x & f(q)=p
Split, 95
97 (p,q) e x'x & f(q)=p => (p,q) e f'
Split, 95
Apply definition of x'x
98 ALL(c2):[(p,c2) e x'x <=> p e x' & c2 e x]
U Spec, 57
99 (p,q) e x'x <=> p e x' & q e x
U Spec, 98
100 [(p,q) e x'x => p e x' & q e x]
& [p e x' & q e x => (p,q) e x'x]
Iff-And, 99
101 (p,q) e x'x => p e x' & q e x
Split, 100
102 p e x' & q e x => (p,q) e x'x
Split, 100
103 p e x' & q e x
Join, 82, 91
104 (p,q) e x'x
Detach, 102, 103
105 (p,q) e x'x & f(q)=p
Join, 104, 92
106 (p,q) e f'
Detach, 97, 105
107 q e x & (p,q) e f'
Join, 91, 106
108 EXIST(d):[d e x & (p,d) e f']
E Gen, 107
As Required:
109 ALL(c):[c e x' => EXIST(d):[d e x & (c,d) e f']]
4 Conclusion, 82
Prove: ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]
Suppose...
110 (p,q1) e f' & (p,q2) e f'
Premise
111 (p,q1) e f'
Split, 110
112 (p,q2) e f'
Split, 110
Apply definition of f'
113 ALL(b):[(p,b) e f' <=> (p,b) e x'x & f(b)=p]
U Spec, 61
114 (p,q1) e f' <=> (p,q1) e x'x & f(q1)=p
U Spec, 113
115 [(p,q1) e f' => (p,q1) e x'x & f(q1)=p]
& [(p,q1) e x'x & f(q1)=p => (p,q1) e f']
Iff-And, 114
116 (p,q1) e f' => (p,q1) e x'x & f(q1)=p
Split, 115
117 (p,q1) e x'x & f(q1)=p => (p,q1) e f'
Split, 115
118 (p,q1) e x'x & f(q1)=p
Detach, 116, 111
119 (p,q1) e x'x
Split, 118
120 f(q1)=p
Split, 118
Apply definition of f'
121 (p,q2) e f' <=> (p,q2) e x'x & f(q2)=p
U Spec, 113
122 [(p,q2) e f' => (p,q2) e x'x & f(q2)=p]
& [(p,q2) e x'x & f(q2)=p => (p,q2) e f']
Iff-And, 121
123 (p,q2) e f' => (p,q2) e x'x & f(q2)=p
Split, 122
124 (p,q2) e x'x & f(q2)=p => (p,q2) e f'
Split, 122
125 (p,q2) e x'x & f(q2)=p
Detach, 123, 112
126 (p,q2) e x'x
Split, 125
127 f(q2)=p
Split, 125
128 f(q1)=f(q2)
Substitute, 127, 120
Apply injective property of f
129 ALL(b):[q1 e x & b e x => [f(q1)=f(b) => q1=b]]
U Spec, 10
130 q1 e x & q2 e x => [f(q1)=f(q2) => q1=q2]
U Spec, 129
131 ALL(c2):[(p,c2) e x'x <=> p e x' & c2 e x]
U Spec, 57
132 (p,q1) e x'x <=> p e x' & q1 e x
U Spec, 131
133 [(p,q1) e x'x => p e x' & q1 e x]
& [p e x' & q1 e x => (p,q1) e x'x]
Iff-And, 132
134 (p,q1) e x'x => p e x' & q1 e x
Split, 133
135 p e x' & q1 e x => (p,q1) e x'x
Split, 133
136 p e x' & q1 e x
Detach, 134, 119
137 p e x'
Split, 136
138 q1 e x
Split, 136
Apply definition of x'x
139 (p,q2) e x'x <=> p e x' & q2 e x
U Spec, 131
140 [(p,q2) e x'x => p e x' & q2 e x]
& [p e x' & q2 e x => (p,q2) e x'x]
Iff-And, 139
141 (p,q2) e x'x => p e x' & q2 e x
Split, 140
142 p e x' & q2 e x => (p,q2) e x'x
Split, 140
143 p e x' & q2 e x
Detach, 141, 126
144 p e x'
Split, 143
145 q2 e x
Split, 143
146 q1 e x & q2 e x
Join, 138, 145
147 f(q1)=f(q2) => q1=q2
Detach, 130, 146
148 q1=q2
Detach, 147, 128
As Required:
149 ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]
4 Conclusion, 110
150 ALL(c):ALL(d):[(c,d) e f' => c e x' & d e x]
& ALL(c):[c e x' => EXIST(d):[d e x & (c,d) e f']]
Join, 81, 109
151 ALL(c):ALL(d):[(c,d) e f' => c e x' & d e x]
& ALL(c):[c e x' => EXIST(d):[d e x & (c,d) e f']]
& ALL(c):ALL(d1):ALL(d2):[(c,d1) e f' & (c,d2) e f' => d1=d2]
Join, 150, 149
f' is a function
As Required:
152 ALL(c):ALL(d):[d=f'(c) <=> (c,d) e f']
Detach, 65, 151
Prove: ALL(a):[a e x' => f'(a) e x]
Suppose...
153 p e x'
Premise
Apply definition of x'
154 p e x' => EXIST(d):[d e x & (p,d) e f']
U Spec, 109
155 EXIST(d):[d e x & (p,d) e f']
Detach, 154, 153
156 q e x & (p,q) e f'
E Spec, 155
157 q e x
Split, 156
158 (p,q) e f'
Split, 156
Apply functionality of f'
159 ALL(d):[d=f'(p) <=> (p,d) e f']
U Spec, 152
160 q=f'(p) <=> (p,q) e f'
U Spec, 159
161 [q=f'(p) => (p,q) e f'] & [(p,q) e f' => q=f'(p)]
Iff-And, 160
162 q=f'(p) => (p,q) e f'
Split, 161
163 (p,q) e f' => q=f'(p)
Split, 161
164 q=f'(p)
Detach, 163, 158
165 f'(p) e x
Substitute, 164, 157
As Required:
166 ALL(a):[a e x' => f'(a) e x]
4 Conclusion, 153
Prove: ALL(a):ALL(b):[a e x' & b e x => [f'(a)=b <=> f(b)=a]]
Suppose...
167 p e x' & q e x
Premise
168 p e x'
Split, 167
169 q e x
Split, 167
Prove: f'(p)=q => f(q)=p
Suppose...
170 f'(p)=q
Premise
Apply functionality of f'
171 ALL(d):[d=f'(p) <=> (p,d) e f']
U Spec, 152
172 q=f'(p) <=> (p,q) e f'
U Spec, 171
173 [q=f'(p) => (p,q) e f'] & [(p,q) e f' => q=f'(p)]
Iff-And, 172
174 q=f'(p) => (p,q) e f'
Split, 173
175 (p,q) e f' => q=f'(p)
Split, 173
176 q=f'(p)
Sym, 170
177 (p,q) e f'
Detach, 174, 176
Apply definition of f'
178 ALL(b):[(p,b) e f' <=> (p,b) e x'x & f(b)=p]
U Spec, 61
179 (p,q) e f' <=> (p,q) e x'x & f(q)=p
U Spec, 178
180 [(p,q) e f' => (p,q) e x'x & f(q)=p]
& [(p,q) e x'x & f(q)=p => (p,q) e f']
Iff-And, 179
181 (p,q) e f' => (p,q) e x'x & f(q)=p
Split, 180
182 (p,q) e x'x & f(q)=p => (p,q) e f'
Split, 180
183 (p,q) e x'x & f(q)=p
Detach, 181, 177
184 (p,q) e x'x
Split, 183
185 f(q)=p
Split, 183
As Required:
186 f'(p)=q => f(q)=p
4 Conclusion, 170
Prove: f(q)=p => f'(p)=q
Suppose...
187 f(q)=p
Premise
Apply definiton of f'
188 ALL(b):[(p,b) e f' <=> (p,b) e x'x & f(b)=p]
U Spec, 61
189 (p,q) e f' <=> (p,q) e x'x & f(q)=p
U Spec, 188
190 [(p,q) e f' => (p,q) e x'x & f(q)=p]
& [(p,q) e x'x & f(q)=p => (p,q) e f']
Iff-And, 189
191 (p,q) e f' => (p,q) e x'x & f(q)=p
Split, 190
Sufficient: (p,q) e f'
192 (p,q) e x'x & f(q)=p => (p,q) e f'
Split, 190
Apply definition of x'x
193 ALL(c2):[(p,c2) e x'x <=> p e x' & c2 e x]
U Spec, 57
194 (p,q) e x'x <=> p e x' & q e x
U Spec, 193
195 [(p,q) e x'x => p e x' & q e x]
& [p e x' & q e x => (p,q) e x'x]
Iff-And, 194
196 (p,q) e x'x => p e x' & q e x
Split, 195
197 p e x' & q e x => (p,q) e x'x
Split, 195
198 p e x' & q e x
Join, 168, 169
199 (p,q) e x'x
Detach, 197, 198
200 (p,q) e x'x & f(q)=p
Join, 199, 187
201 (p,q) e f'
Detach, 192, 200
Apply functionality of f'
202 ALL(d):[d=f'(p) <=> (p,d) e f']
U Spec, 152
203 q=f'(p) <=> (p,q) e f'
U Spec, 202
204 [q=f'(p) => (p,q) e f'] & [(p,q) e f' => q=f'(p)]
Iff-And, 203
205 q=f'(p) => (p,q) e f'
Split, 204
206 (p,q) e f' => q=f'(p)
Split, 204
207 q=f'(p)
Detach, 206, 201
208 f'(p)=q
Sym, 207
As Required:
209 f(q)=p => f'(p)=q
4 Conclusion, 187
210 [f'(p)=q => f(q)=p] & [f(q)=p => f'(p)=q]
Join, 186, 209
211 f'(p)=q <=> f(q)=p
Iff-And, 210
As Required:
212 ALL(a):ALL(b):[a e x' & b e x => [f'(a)=b <=> f(b)=a]]
4 Conclusion, 167
Prove: ALL(a):ALL(b):[a e x' & b e x' => [f'(a)=f'(b) => a=b]]
Suppose...
213 p e x' & q e x'
Premise
214 p e x'
Split, 213
215 q e x'
Split, 213
Prove: f'(p)=f'(q) => p=q
Suppose...
216 f'(p)=f'(q)
Premise
Apply property of f'
217 ALL(b):[p e x' & b e x => [f'(p)=b <=> f(b)=p]]
U Spec, 212
218 p e x' & f'(q) e x => [f'(p)=f'(q) <=> f(f'(q))=p]
U Spec, 217
219 q e x' => f'(q) e x
U Spec, 166
220 f'(q) e x
Detach, 219, 215
221 p e x' & f'(q) e x
Join, 214, 220
222 f'(p)=f'(q) <=> f(f'(q))=p
Detach, 218, 221
223 [f'(p)=f'(q) => f(f'(q))=p]
& [f(f'(q))=p => f'(p)=f'(q)]
Iff-And, 222
224 f'(p)=f'(q) => f(f'(q))=p
Split, 223
225 f(f'(q))=p => f'(p)=f'(q)
Split, 223
226 f(f'(q))=p
Detach, 224, 216
Apply property of f'
227 ALL(b):[q e x' & b e x => [f'(q)=b <=> f(b)=q]]
U Spec, 212
228 q e x' & f'(q) e x => [f'(q)=f'(q) <=> f(f'(q))=q]
U Spec, 227
229 q e x' => f'(q) e x
U Spec, 166
230 f'(q) e x
Detach, 229, 215
231 q e x' & f'(q) e x
Join, 215, 230
232 f'(q)=f'(q) <=> f(f'(q))=q
Detach, 228, 231
233 [f'(q)=f'(q) => f(f'(q))=q]
& [f(f'(q))=q => f'(q)=f'(q)]
Iff-And, 232
234 f'(q)=f'(q) => f(f'(q))=q
Split, 233
235 f(f'(q))=q => f'(q)=f'(q)
Split, 233
236 f'(q)=f'(q)
Reflex
237 f(f'(q))=q
Detach, 234, 236
238 p=q
Substitute, 226, 237
As Required:
239 f'(p)=f'(q) => p=q
4 Conclusion, 216
f' is injective (1-1)
As Required:
240 ALL(a):ALL(b):[a e x' & b e x' => [f'(a)=f'(b) => a=b]]
4 Conclusion, 213
Prove: ALL(a):[aex => EXIST(b):[bex' & f'(b)=a]]
Use b=f(a)
Suppose...
241 p e x
Premise
Apply definition of x'
242 f(p) e x' <=> f(p) e x & EXIST(b):[b e x & f(b)=f(p)]
U Spec, 26
243 [f(p) e x' => f(p) e x & EXIST(b):[b e x & f(b)=f(p)]]
& [f(p) e x & EXIST(b):[b e x & f(b)=f(p)] => f(p) e x']
Iff-And, 242
244 f(p) e x' => f(p) e x & EXIST(b):[b e x & f(b)=f(p)]
Split, 243
245 f(p) e x & EXIST(b):[b e x & f(b)=f(p)] => f(p) e x'
Split, 243
246 p e x => f(p) e x
U Spec, 9
247 f(p) e x
Detach, 246, 241
248 f(p)=f(p)
Reflex
249 p e x & f(p)=f(p)
Join, 241, 248
250 EXIST(b):[b e x & f(b)=f(p)]
E Gen, 249
251 f(p) e x & EXIST(b):[b e x & f(b)=f(p)]
Join, 247, 250
252 f(p) e x'
Detach, 245, 251
Apply property of f'
253 ALL(b):[f(p) e x' & b e x => [f'(f(p))=b <=> f(b)=f(p)]]
U Spec, 212
254 f(p) e x' & p e x => [f'(f(p))=p <=> f(p)=f(p)]
U Spec, 253
255 f(p) e x' & p e x
Join, 252, 241
256 f'(f(p))=p <=> f(p)=f(p)
Detach, 254, 255
257 [f'(f(p))=p => f(p)=f(p)] & [f(p)=f(p) => f'(f(p))=p]
Iff-And, 256
258 f'(f(p))=p => f(p)=f(p)
Split, 257
259 f(p)=f(p) => f'(f(p))=p
Split, 257
260 f'(f(p))=p
Detach, 259, 248
261 f(p) e x' & f'(f(p))=p
Join, 252, 260
262 EXIST(b):[b e x' & f'(b)=p]
E Gen, 261
f' is surjective
As Required:
263 ALL(a):[a e x => EXIST(b):[b e x' & f'(b)=a]]
4 Conclusion, 241
Joining results...
264 Set(x') & ALL(a):[a e x' => a e x]
Join, 25, 34
265 Set(x') & ALL(a):[a e x' => a e x]
& EXIST(a):[a e x & ~a e x']
Join, 264, 49
266 Set(x') & ALL(a):[a e x' => a e x]
& EXIST(a):[a e x & ~a e x']
& ALL(a):[a e x' => f'(a) e x]
Join, 265, 166
267 Set(x') & ALL(a):[a e x' => a e x]
& EXIST(a):[a e x & ~a e x']
& 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]]
Join, 266, 240
268 Set(x') & ALL(a):[a e x' => a e x]
& EXIST(a):[a e x & ~a e x']
& 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]]
& ALL(a):[a e x => EXIST(b):[b e x' & f'(b)=a]]
Join, 267, 263
269 EXIST(f):[Set(x') & ALL(a):[a e x' => a e x]
& EXIST(a):[a e x & ~a e x']
& 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]]
& ALL(a):[a e x => EXIST(b):[b e x' & f(b)=a]]]
E Gen, 268
270 EXIST(s'):EXIST(f):[Set(s') & ALL(a):[a e s' => a e x]
& EXIST(a):[a e x & ~a e s']
& ALL(a):[a e s' => f(a) e x]
& ALL(a):ALL(b):[a e s' & b e s' => [f(a)=f(b) => a=b]]
& ALL(a):[a e x => EXIST(b):[b e s' & f(b)=a]]]
E Gen, 269
x is infinite
271 Infinite(x)
Detach, 7, 270
As Required:
272 ~ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
=> Infinite(x)
4 Conclusion, 11
Apply Contrapositive Rule
273 ~Infinite(x) => ~~ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
Contra, 272
274 ~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
Rem DNeg, 273
As Required:
275 ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]
4 Conclusion, 8
As Required:
276 ALL(x):[Set(x)
=> ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]]
4 Conclusion, 2
Prove: ALL(x):ALL(f):[Set(x)
& ~Infinite(x)
& 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]]
=> ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]
Suppose...
277 Set(x)
& ~Infinite(x)
& 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]]
Premise
278 Set(x)
Split, 277
279 ~Infinite(x)
Split, 277
280 ALL(a):[a e x => f(a) e x]
Split, 277
281 ALL(a):ALL(b):[a e x & b e x => [f(a)=f(b) => a=b]]
Split, 277
Apply previous result
282 Set(x)
=> ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]
U Spec, 276
283 ALL(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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]]
Detach, 282, 278
284 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]]
=> [~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]
U Spec, 283
285 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]]
Join, 280, 281
286 ~Infinite(x) => ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
Detach, 284, 285
287 ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]
Detach, 286, 279
As Required:
288 ALL(x):ALL(f):[Set(x)
& ~Infinite(x)
& 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]]
=> ALL(a):[a e x => EXIST(b):[b e x & f(b)=a]]]
4 Conclusion, 277