LEMMA 3  (Cantor's Theorem)

*******

Suppose p is the power set of s.

Then there exists no surjection f: s --> p.

(This proof was prepared with the use of the author's DC Proof 2.0 software available at http://www.dcproof.com )

OUTLINE

*******

Suppose p is the power set of s.

Suppose to contrary that there exists surjection f mapping s onto p, and obtain a contradiction.

Construct subset k of s such that for each element x, we have ~x e f(x).

We have k e s. Let k' be the pre-image of k. Derive the contradiction k' e k and ~k' e k.

DEFINITIONS

***********

Define: Surjection

1 ALL(f):ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]

Axiom

     PROOF OF LEMMA 3

     ****************

     Suppose p is the power set of s

2 Set(s)

          & Set(p)

          & ALL(c):[c e p <=> Set(c) & ALL(d):[d e c => d e s]]

Premise

3 Set(s)

Split, 2

     Define: p  (power set of s)

4 Set(p)

Split, 2

5 ALL(c):[c e p <=> Set(c) & ALL(d):[d e c => d e s]]

Split, 2

          Prove there exists no surjection mapping s to p.

          Suppose f is a function mapping s to p.

6 ALL(a):[a e s => f(a) e p]

Premise

              Prove f is not a surjection.

              Suppose to the contrary that f is a surjection, and obtain a contradiction.

7 Surjection(f,s,p)

Premise

              Apply definition of Surjection

8 ALL(a):ALL(b):[Surjection(f,a,b) <=> ALL(c):[c e b => EXIST(d):[d e a & f(d)=c]]]

U Spec, 1

9 ALL(b):[Surjection(f,s,b) <=> ALL(c):[c e b => EXIST(d):[d e s & f(d)=c]]]

U Spec, 8

10 Surjection(f,s,p) <=> ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]]

U Spec, 9

11 [Surjection(f,s,p) => ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]]]

                   & [ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,p)]

Iff-And, 10

12 Surjection(f,s,p) => ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]]

Split, 11

13 ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]] => Surjection(f,s,p)

Split, 11

14 ALL(c):[c e p => EXIST(d):[d e s & f(d)=c]]

Detach, 12, 7

               Construct subset k of s such that for each element x, we have ~x e f(x).

               Apply Subset Axiom.

15 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e s & ~a e f(a)]]

Subset, 3

16 Set(k) & ALL(a):[a e k <=> a e s & ~a e f(a)]

E Spec, 15

               Define: k

17 Set(k)

Split, 16

18 ALL(a):[a e k <=> a e s & ~a e f(a)]

Split, 16

              Prove: k e p

              Apply definition of p

19 k e p <=> Set(k) & ALL(d):[d e k => d e s]

U Spec, 5

20 [k e p => Set(k) & ALL(d):[d e k => d e s]]

                   & [Set(k) & ALL(d):[d e k => d e s] => k e p]

Iff-And, 19

21 k e p => Set(k) & ALL(d):[d e k => d e s]

Split, 20

              Sufficient: For  k e p

22 Set(k) & ALL(d):[d e k => d e s] => k e p

Split, 20

                   Prove k is a subset of s

                   Suppose...

23 x e k

Premise

                   Apply definition of k

24 x e k <=> x e s & ~x e f(x)

U Spec, 18

25 [x e k => x e s & ~x e f(x)]

                        & [x e s & ~x e f(x) => x e k]

Iff-And, 24

26 x e k => x e s & ~x e f(x)

                Split, 25

27 x e s & ~x e f(x) => x e k

Split, 25

28 x e s & ~x e f(x)

Detach, 26, 23

29 x e s

Split, 28

              As Required:

30 ALL(d):[d e k => d e s]

4 Conclusion, 23

31 Set(k) & ALL(d):[d e k => d e s]

Join, 17, 30

              As Required:

32 k e p

Detach, 22, 31

              Find pre-image of k under f.

              Apply surjectivity of f.

33 k e p => EXIST(d):[d e s & f(d)=k]

U Spec, 14

34 EXIST(d):[d e s & f(d)=k]

Detach, 33, 32

35 k' e s & f(k')=k

E Spec, 34

              Define: k'  (the pre-image of k under f)

36 k' e s

Split, 35

37 f(k')=k

Split, 35

              Determine whether k' e k.

              Apply definition of k.

38 k' e k <=> k' e s & ~k' e f(k')

U Spec, 18

39 k' e k <=> k' e s & ~k' e k

Substitute, 37, 38

40 [k' e k => k' e s & ~k' e k]

                   & [k' e s & ~k' e k => k' e k]

Iff-And, 39

41 k' e k => k' e s & ~k' e k

Split, 40

42 k' e s & ~k' e k => k' e k

Split, 40

                   Prove: ~k' e k

                   Suppose to the contrary...

43 k' e k

Premise

44 k' e s & ~k' e k

Detach, 41, 43

45 k' e s

Split, 44

46 ~k' e k

Split, 44

47 k' e k & ~k' e k

Join, 43, 46

              As Required:

48 ~k' e k

4 Conclusion, 43

              Prove: k' e k  (to obtain a contradiction)

49 k' e s & ~k' e k

Join, 36, 48

50 k' e k

Detach, 42, 49

              We have the contradiction...

51 k' e k & ~k' e k

Join, 50, 48

          As Required:

52 ~Surjection(f,s,p)

4 Conclusion, 7

     As Required:

53 ALL(f):[ALL(a):[a e s => f(a) e p] => ~Surjection(f,s,p)]

4 Conclusion, 6

As Required:

54 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)]]

4 Conclusion, 2