LEMMA 5
*******
Suppose ps be the power set of s.
Then there exists no injective f: ps --> s.
(This proof was written with the aid of author's DC Proof 2.0 software available at http://www.dcproof.com )
OUTLINE
*******
Suppose to the contrary that there exists injective f: ps --> s.
By Lemma 4, there would then exist surjective g: s --> ps.
This contradicts Lemma 3 (Cantor's Theorem).
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
PREVIOUS RESULTS (with links to proofs)
****************
Lemma 4: Proof
Suppose we have an injective (one-to-one) function mapping of non-empty set x to set y.
Then there exists a surjective (onto) function mapping y to x.
3 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
Lemma 3: (Cantor's Theorem) Proof
Suppose ps is the power set of s.
Then there exists no surjective (onto) function mapping s to ps.
4 ALL(s):ALL(p):[Set(s)
& Set(p)
& ALL(c):[c e p <=> Set(c) & ALL(d):[d e c => d e s]]
=> ALL(f):[ALL(a):[a e s => f(a) e p] => ~Surjection(f,s,p)]]
Axiom
PROOF OF LEMMA 5
****************
Suppose ps is the power set of s
5 Set(s)
& Set(ps)
& ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
Premise
6 Set(s)
Split, 5
7 Set(ps)
Split, 5
8 ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
Split, 5
Prove there exists no injective (one-to-one) function f mapping ps to s.
Suppose to the contrary...
9 EXIST(f):[ALL(c):[c e ps => f(c) e s] & Injection(f,ps,s)]
Premise
10 ALL(c):[c e ps => f(c) e s] & Injection(f,ps,s)
E Spec, 9
Define: f
11 ALL(c):[c e ps => f(c) e s]
Split, 10
12 Injection(f,ps,s)
Split, 10
To apply Lemma 2, we must show that ps is non-empty. We will show that the empty set is itself an
element of ps.
Construct phi (the empty set).
Apply the Subset Axiom.
13 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e s]]
Subset, 6
14 Set(phi) & ALL(a):[a e phi <=> a e s & ~a e s]
E Spec, 13
Define: phi
15 Set(phi)
Split, 14
16 ALL(a):[a e phi <=> a e s & ~a e s]
Split, 14
Prove: phi e ps (ps is not empty)
Apply definition of ps
17 phi e ps <=> Set(phi) & ALL(d):[d e phi => d e s]
U Spec, 8
18 [phi e ps => Set(phi) & ALL(d):[d e phi => d e s]]
& [Set(phi) & ALL(d):[d e phi => d e s] => phi e ps]
Iff-And, 17
19 phi e ps => Set(phi) & ALL(d):[d e phi => d e s]
Split, 18
Sufficient: For phi e ps
20 Set(phi) & ALL(d):[d e phi => d e s] => phi e ps
Split, 18
Prove: ~EXIST(a):a e phi
Suppose to the contrary...
21 x e phi
Premise
Apply defintion of phi
22 x e phi <=> x e s & ~x e s
U Spec, 16
23 [x e phi => x e s & ~x e s]
& [x e s & ~x e s => x e phi]
Iff-And, 22
24 x e phi => x e s & ~x e s
Split, 23
25 x e s & ~x e s => x e phi
Split, 23
26 x e s & ~x e s
Detach, 24, 21
As Required:
27 ~EXIST(a):a e phi
4 Conclusion, 21
Changing quantfier...
28 ~~ALL(a):~a e phi
Quant, 27
Alternatively...
29 ALL(a):~a e phi
Rem DNeg, 28
Prove phi is a subset of s
Suppose...
30 x e phi
Premise
31 ~x e phi
U Spec, 29
32 ~~x e phi => x e s
Arb Cons, 31
33 x e phi => x e s
Rem DNeg, 32
34 x e s
Detach, 33, 30
As Required:
35 ALL(d):[d e phi => d e s]
4 Conclusion, 30
36 Set(phi) & ALL(d):[d e phi => d e s]
Join, 15, 35
37 phi e ps
Detach, 20, 36
As Required:
ps is non-empty
38 EXIST(a):a e ps
E Gen, 37
Prove g must be a surjection mapping s to ps
Apply Lemma 2
39 ALL(b):ALL(f1):[Set(ps)
& Set(b)
& EXIST(c):c e ps
& ALL(c):[c e ps => f1(c) e b]
& Injection(f1,ps,b)
=> EXIST(f2):[ALL(c):[c e b => f2(c) e ps] & Surjection(f2,b,ps)]]
U Spec, 3
40 ALL(f1):[Set(ps)
& Set(s)
& EXIST(c):c e ps
& ALL(c):[c e ps => f1(c) e s]
& Injection(f1,ps,s)
=> EXIST(f2):[ALL(c):[c e s => f2(c) e ps] & Surjection(f2,s,ps)]]
U Spec, 39
41 Set(ps)
& Set(s)
& EXIST(c):c e ps
& ALL(c):[c e ps => f(c) e s]
& Injection(f,ps,s)
=> EXIST(f2):[ALL(c):[c e s => f2(c) e ps] & Surjection(f2,s,ps)]
U Spec, 40
42 Set(ps) & Set(s)
Join, 7, 6
43 Set(ps) & Set(s) & EXIST(a):a e ps
Join, 42, 38
44 Set(ps) & Set(s) & EXIST(a):a e ps
& ALL(c):[c e ps => f(c) e s]
Join, 43, 11
45 Set(ps) & Set(s) & EXIST(a):a e ps
& ALL(c):[c e ps => f(c) e s]
& Injection(f,ps,s)
Join, 44, 12
46 EXIST(f2):[ALL(c):[c e s => f2(c) e ps] & Surjection(f2,s,ps)]
Detach, 41, 45
47 ALL(c):[c e s => g(c) e ps] & Surjection(g,s,ps)
E Spec, 46
48 ALL(c):[c e s => g(c) e ps]
Split, 47
As Required:
g is a surjection mapping s to ps
49 Surjection(g,s,ps)
Split, 47
Prove: ~Surjection(g,s,ps) to obtain a contradiction
Apply Lemma 3
50 ALL(p):[Set(s)
& Set(p)
& ALL(c):[c e p <=> Set(c) & ALL(d):[d e c => d e s]]
=> ALL(f):[ALL(a):[a e s => f(a) e p] => ~Surjection(f,s,p)]]
U Spec, 4
51 Set(s)
& Set(ps)
& ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
=> ALL(f):[ALL(a):[a e s => f(a) e ps] => ~Surjection(f,s,ps)]
U Spec, 50
52 ALL(f):[ALL(a):[a e s => f(a) e ps] => ~Surjection(f,s,ps)]
Detach, 51, 5
53 ALL(a):[a e s => g(a) e ps] => ~Surjection(g,s,ps)
U Spec, 52
As Required:
54 ~Surjection(g,s,ps)
Detach, 53, 48
Obtain contradiction...
55 Surjection(g,s,ps) & ~Surjection(g,s,ps)
Join, 49, 54
As Required:
56 ~EXIST(f):[ALL(c):[c e ps => f(c) e s] & Injection(f,ps,s)]
4 Conclusion, 9
As Required:
57 ALL(s):ALL(ps):[Set(s)
& Set(ps)
& ALL(c):[c e ps <=> Set(c) & ALL(d):[d e c => d e s]]
=> ~EXIST(f):[ALL(c):[c e ps => f(c) e s] & Injection(f,ps,s)]]
4 Conclusion, 5