This theorem states that any set is
strictly less numerous than its power set.
Proof sketch
First, it must be shown that an injection i: X →
power X exists. This is easily witnessed by i x := {x}, since we have
sg_is_inj. Now it must be shown that no surjection
f: X → power X exists. So let f be such a surjection; we need to find
a contradiction. Consider the "diagonal" set
D = {x ∈ X | x ∉ f x}.
Because D ⊆ X, we have D ∈ power X. Furthermore, because f is
surjective, we have D ∈ rng f. So there is an x ∈ X with
D = f x. Since x ∈ X, we obtain the equivalence
x ∈ D ↔ x ∉ f x
directly from the Definition of D. Thus
x ∈ f x ↔ x ∉ f x,
but this is a contradiction, as shown in diag_contra. q.e.d.
Proof
let i = {t | ∃x. x ∈ X ∧ t = (x, {x})}.
01. ⊢ i = i, eq_refl.
02. 2 ⊢ x ∈ X, hypo.
03. 2 ⊢ {x} ⊆ X, sg_incl_in 2.
04. 2 ⊢ set x, set_intro 2.
05. 2 ⊢ set {x}, set_sg 4.
06. 2 ⊢ {x} ∈ power X, power_intro 5 3.
07. ⊢ x ∈ X → {x} ∈ power X, subj_intro 6.
08. ⊢ ∀x. x ∈ X → {x} ∈ power X, uq_intro 7.
09. ⊢ map i X (power X), map_from_term 1 8.
10. 10 ⊢ a ∈ X, hypo.
11. 11 ⊢ b ∈ X, hypo.
12. 12 ⊢ app i a = app i b, hypo.
13. 10 ⊢ app i a = {a}, map_from_term_app 1 8 10.
14. 11 ⊢ app i b = {b}, map_from_term_app 1 8 11.
15. 11, 12 ⊢ app i a = {b}, eq_trans 12 14.
16. 10, 11, 12 ⊢ {a} = {b}, eq_trans_ll 13 15.
17. 10 ⊢ set a, set_intro 10.
18. 11 ⊢ set b, set_intro 11.
19. 10, 11, 12 ⊢ a = b, sg_is_inj 17 18 16.
20. ⊢ a ∈ X → b ∈ X → app i a = app i b → a = b, subj_intro_iii 19.
21. ⊢ ∀b. a ∈ X → b ∈ X → app i a = app i b → a = b, uq_intro 20.
22. ⊢ ∀a. ∀b. a ∈ X → b ∈ X → app i a = app i b → a = b, uq_intro 21.
23. ⊢ inj i X (power X), inj_intro 9 22.
24. ⊢ ∃g. inj g X (power X), ex_intro 23.
let D = {x | x ∈ X ∧ ¬x ∈ app f x}.
25. 25 ⊢ set X, hypo.
26. 26 ⊢ ∃f. sur f X (power X), hypo.
27. 27 ⊢ sur f X (power X), hypo.
28. ⊢ D ⊆ X, sep_is_subclass.
29. 25 ⊢ set D, subset 28 25.
30. 25 ⊢ D ∈ power X, power_intro 29 28.
31. 27 ⊢ rng f = power X, sur_elim 27.
32. 25, 27 ⊢ D ∈ rng f, eq_subst_rev 31 30, P t ↔ D ∈ t.
33. 27 ⊢ map f X (power X), sur_is_map 27.
34. 25, 27 ⊢ ∃x. x ∈ X ∧ D = app f x, map_rng_elim 33 32.
35. 35 ⊢ x ∈ X ∧ D = app f x, hypo.
36. 35 ⊢ x ∈ X, conj_eliml 35.
37. 35 ⊢ D = app f x, conj_elimr 35.
38. ⊢ x ∈ D ↔ x ∈ D, equi_refl.
39. 35 ⊢ x ∈ app f x ↔ x ∈ D, eq_subst 37 38, P t ↔ (x ∈ t ↔ x ∈ D).
40. 40 ⊢ x ∈ D, hypo.
41. 40 ⊢ x ∈ X ∧ ¬x ∈ app f x, comp_elim 40.
42. 40 ⊢ ¬x ∈ app f x, conj_elimr 41.
43. ⊢ x ∈ D → ¬x ∈ app f x, subj_intro 42.
44. 44 ⊢ ¬x ∈ app f x, hypo.
45. 35, 44 ⊢ x ∈ X ∧ ¬x ∈ app f x, conj_intro 36 44.
46. 35 ⊢ set x, set_intro 36.
47. 35, 44 ⊢ x ∈ D, comp_intro 46 45.
48. 35 ⊢ ¬x ∈ app f x → x ∈ D, subj_intro 47.
49. 35 ⊢ x ∈ D ↔ ¬x ∈ app f x, bij_intro 43 48.
50. 35 ⊢ x ∈ app f x ↔ ¬x ∈ app f x, equi_trans 39 49.
51. 35 ⊢ ⊥, diag_contra 50.
52. 25, 27 ⊢ ⊥, ex_elim 34 51.
53. 25, 26 ⊢ ⊥, ex_elim 26 52.
54. 25 ⊢ ¬∃f. sur f X (power X), neg_intro 53.
55. ⊢ num_le X (power X), num_le_intro 24.
56. 25 ⊢ num_lt X (power X), num_lt_intro 55 54.
Cantor's_theorem. ⊢ set X → num_lt X (power X), subj_intro 56.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.