THEOREM
*******
ALL(s):[Set(s) & EXIST(a):a e s
=> [Countable(s) => EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]]
(This formal proof was write and verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com )
PREVIOUS RESULTS
****************
Injective function f1: A --> B for non-empty A, implies existence of surjective f1: B --> A (See proof)
1 ALL(a):ALL(b):ALL(f1):[Set(a) & Set(b) & EXIST(c):c e a & ALL(c):[c e a => f1(c) e b]
& Injection(f1,a,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e a] & Surjection(f2,b,a)]]
Axiom
DEFINITIONS
***********
Let n be the set of natural numbers
2 Set(n)
Axiom
Define: Countable
*****************
3 ALL(s):[Set(s) => [Countable(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]]]
Axiom
Define: Surjection
******************
4 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: Injection
*****************
5 ALL(f):ALL(a):ALL(b):[Injection(f,a,b) <=> ALL(c):ALL(d):[c e a & d e b => [f(c)=f(d)
=> c=d]]]
Axiom
PROOF
*****
Prove: ALL(s):[Set(s) & EXIST(a):a e s
=> [Countable(s) => EXIST(f):[ALL(a):[a e n => a e s] & Surjection(f,n,s)]]]
Suppose...
6 Set(s) & EXIST(a):a e s
Premise
7 Set(s)
Split, 6
8 EXIST(a):a e s
Split, 6
Define: x0
9 x0 e s
E Spec, 8
Prove: Countable(s) => EXIST(f):[ALL(a):[a e n => a e s] & Surjection(f,n,s)]]
Suppose...
10 Countable(s)
Premise
11 Set(s) => [Countable(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]]
U Spec, 3
12 Countable(s)
<=> EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]
Detach, 11, 7
13 [Countable(s) => EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]]
& [EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)] => Countable(s)]
Iff-And, 12
14 Countable(s) => EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]
Split, 13
15 EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)] => Countable(s)
Split, 13
16 EXIST(f):[ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)]
Detach, 14, 10
17 ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)
E Spec, 16
18 ALL(b):[b e s => f(b) e n]
Split, 17
19 Injection(f,s,n)
Split, 17
20 ALL(b):ALL(f1):[Set(s) & Set(b) & EXIST(c):c e s & ALL(c):[c e s
=> f1(c) e b] & Injection(f1,s,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e s] & Surjection(f2,b,s)]]
U Spec, 1
21 ALL(f1):[Set(s) & Set(n) & EXIST(c):c e s & ALL(c):[c e s => f1(c) e n]
& Injection(f1,s,n)
=> EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]
U Spec, 20
22 Set(s) & Set(n) & EXIST(c):c e s & ALL(c):[c e s => f(c) e n] & Injection(f,s,n)
=> EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]
U Spec, 21
23 Set(s) & Set(n)
Join, 7, 2
24 Set(s) & Set(n) & EXIST(a):a e s
Join, 23, 8
25 Set(s) & Set(n) & EXIST(a):a e s
& ALL(b):[b e s => f(b) e n]
Join, 24, 18
26 Set(s) & Set(n) & EXIST(a):a e s
& ALL(b):[b e s => f(b) e n]
& Injection(f,s,n)
Join, 25, 19
27 EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]
Detach, 22, 26
28 Countable(s)
=> EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]
4 Conclusion, 10
As Required:
29 ALL(s):[Set(s) & EXIST(a):a e s
=> [Countable(s)
=> EXIST(f2):[ALL(c):[c e n => f2(c) e s] & Surjection(f2,n,s)]]]
4 Conclusion, 6