This theorem states that the power set of a set X is
equinumerous to set of maps
from X to {0, 1}.
Proof sketch
Equinumerousity of two sets means that there
is a bijection between them. We have the canonical bijection
φ: power X → Map X {0, 1}, φ A := χA,
where χA is the indicator function of A.
First we need to show that φ is injective. So let A, B be two arbritary
sets in the domain. Assume φ A = φ B. By definition of φ this means
χA = χB. Let x ∈ A. Then χA = 1,
thus χB = 1, and therefore x ∈ B. In the same way,
x ∈ A is derived from x ∈ B. Thus A = B by extensionality.
Now we need to show that φ is surjective. So let f be an arbritary
element in the codomain. We need to find an A with φ A = f.
Let A := f−1{1}, the "one-fiber" of f.
So we need to show χA x = f x for an arbritary x ∈ X,
then χA = f holds by function extensionality.
There are only two cases for the value of f. In the case f x = 1, it
holds that x ∈ A, since A has just been defined this way. So
χA x = 1, thus χA x = f x, as desired.
In the case f x = 0, it holds that x ∈ X \ A, for the same reason.
So χA x = 0, thus χA x = f x,
as desired. q.e.d.
Proof
let φ = {t | ∃A. A ∈ power X ∧ t = (A, χ A X)}.
01. 1 ⊢ set X, hypo.
02. 2 ⊢ A ∈ power X, hypo.
03. 2 ⊢ A ⊆ X, power_elim 2.
04. 2 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 3.
05. 1, 2 ⊢ χ A X ∈ Map X {∅, {∅}}, Map_intro 4 1.
06. 1 ⊢ A ∈ power X → χ A X ∈ Map X {∅, {∅}}, subj_intro 5.
07. 1 ⊢ ∀A. A ∈ power X → χ A X ∈ Map X {∅, {∅}}, uq_intro 6.
08. ⊢ φ = φ, eq_refl.
09. 1 ⊢ map φ (power X) (Map X {∅, {∅}}), map_from_term 8 7.
10. 10 ⊢ A ∈ power X, hypo.
11. 11 ⊢ B ∈ power X, hypo.
12. 12 ⊢ app φ A = app φ B, hypo.
13. 1, 10 ⊢ app φ A = χ A X, map_from_term_app 8 7 10.
14. 1, 11 ⊢ app φ B = χ B X, map_from_term_app 8 7 11.
15. 1, 10, 12 ⊢ χ A X = app φ B, eq_trans_ll 13 12.
16. 1, 10, 11, 12 ⊢ χ A X = χ B X, eq_trans 15 14.
17. 10 ⊢ A ⊆ X, power_elim 10.
18. 11 ⊢ B ⊆ X, power_elim 11.
19. 19 ⊢ x ∈ A, hypo.
20. 10, 19 ⊢ app (χ A X) x = {∅}, indicator_app_is_one 17 19.
21. 1, 10, 11, 12, 19 ⊢ app (χ B X) x = {∅},
eq_subst 16 20, P t ↔ app t x = {∅}.
22. 10, 19 ⊢ x ∈ X, incl_elim 17 19.
23. 1, 10, 11, 12, 19 ⊢ x ∈ B, from_indicator_app_is_one 18 22 21.
24. 1, 10, 11, 12 ⊢ x ∈ A → x ∈ B, subj_intro 23.
25. 25 ⊢ x ∈ B, hypo.
26. 11, 25 ⊢ app (χ B X) x = {∅}, indicator_app_is_one 18 25.
27. 1, 10, 11, 12, 25 ⊢ app (χ A X) x = {∅},
eq_subst_rev 16 26, P t ↔ app t x = {∅}.
28. 11, 25 ⊢ x ∈ X, incl_elim 18 25.
29. 1, 10, 11, 12, 25 ⊢ x ∈ A, from_indicator_app_is_one 17 28 27.
30. 1, 10, 11, 12 ⊢ x ∈ B → x ∈ A, subj_intro 29.
31. 1, 10, 11, 12 ⊢ x ∈ A ↔ x ∈ B, bij_intro 24 30.
32. 1, 10, 11, 12 ⊢ ∀x. x ∈ A ↔ x ∈ B, uq_intro 31.
33. 1, 10, 11, 12 ⊢ A = B, ext 32.
34. 1 ⊢ A ∈ power X → B ∈ power X → app φ A = app φ B → A = B,
subj_intro_iii 33.
35. 1 ⊢ ∀B. A ∈ power X → B ∈ power X →
app φ A = app φ B → A = B, uq_intro 34.
36. 1 ⊢ ∀A. ∀B. A ∈ power X → B ∈ power X →
app φ A = app φ B → A = B, uq_intro 35.
37. 1 ⊢ inj φ (power X) (Map X {∅, {∅}}), inj_intro 9 36.
let A = inv_img f {{∅}}.
38. 38 ⊢ f ∈ Map X {∅, {∅}}, hypo.
39. 38 ⊢ map f X {∅, {∅}}, Map_elim 38.
40. 38 ⊢ function f ∧ dom f = X ∧ rng f ⊆ {∅, {∅}}, map_unfold 39.
41. 38 ⊢ dom f = X, conj_elimlr 40.
42. 42 ⊢ x ∈ X, hypo.
43. 38, 42 ⊢ app f x ∈ {∅, {∅}}, map_app_in_cod 39 42.
44. 38, 42 ⊢ app f x ∈ {∅} ∨ app f x ∈ {{∅}}, union_elim 43.
45. 45 ⊢ app f x ∈ {∅}, hypo.
46. 45 ⊢ app f x = ∅, sg_elim empty_set_is_set 45.
47. 45 ⊢ ∅ = app f x, eq_symm 46.
48. 38, 42, 45 ⊢ (x, ∅) ∈ f, map_app_elim 39 42 47.
49. ⊢ A ⊆ dom f, inv_img_incl_in_dom.
50. 38 ⊢ A ⊆ X, eq_subst 41 49, P t ↔ A ⊆ t.
51. 51 ⊢ x ∈ A, hypo.
52. 51 ⊢ ∃y. y ∈ {{∅}} ∧ (x, y) ∈ f, inv_img_elim 51.
53. 53 ⊢ y ∈ {{∅}} ∧ (x, y) ∈ f, hypo.
54. 53 ⊢ y ∈ {{∅}}, conj_eliml 53.
55. 53 ⊢ (x, y) ∈ f, conj_elimr 53.
56. 38 ⊢ function f, conj_elimll 40.
57. 38, 42, 45, 53 ⊢ y = ∅, fn_unique_value 56 55 48.
58. ⊢ set {∅}, set_sg empty_set_is_set.
59. 53 ⊢ y = {∅}, sg_elim 58 54.
60. 38, 42, 45, 53 ⊢ ∅ = {∅}, eq_trans_ll 57 59.
61. 38, 42, 45, 53 ⊢ ⊥, neg_elim zero_neq_one 60.
62. 38, 42, 45, 51 ⊢ ⊥, ex_elim 52 61.
63. 38, 42, 45 ⊢ ¬x ∈ A, neg_intro 62.
64. 38, 42, 45 ⊢ x ∈ X \ A, diff_intro 42 63.
65. 38, 42, 45 ⊢ app (χ A X) x = ∅, indicator_app_is_zero 50 64.
66. 38, 42, 45 ⊢ ∅ = app (χ A X) x, eq_symm 65.
67. 38, 42, 45 ⊢ app f x = app (χ A X) x, eq_trans 46 66.
68. 68 ⊢ app f x ∈ {{∅}}, hypo.
69. 68 ⊢ app f x = {∅}, sg_elim 58 68.
70. 68 ⊢ {∅} = app f x, eq_symm 69.
71. 38, 42, 68 ⊢ (x, {∅}) ∈ f, map_app_elim 39 42 70.
72. ⊢ {∅} = {∅}, eq_refl.
73. ⊢ {∅} ∈ {{∅}}, sg_intro 58 72.
74. 38, 42, 68 ⊢ x ∈ A, inv_img_intro 73 71.
75. 38, 42, 68 ⊢ app (χ A X) x = {∅}, indicator_app_is_one 50 74.
76. 38, 42, 68 ⊢ {∅} = app (χ A X) x, eq_symm 75.
77. 38, 42, 68 ⊢ app f x = app (χ A X) x, eq_trans 69 76.
78. 38, 42 ⊢ app f x = app (χ A X) x, disj_elim 44 67 77.
79. 38 ⊢ x ∈ X → app f x = app (χ A X) x, subj_intro 78.
80. 38 ⊢ ∀x. x ∈ X → app f x = app (χ A X) x, uq_intro 79.
81. 38 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 50.
82. 38 ⊢ f = χ A X, map_extensionality 39 81 80.
83. 1, 38 ⊢ set A, subset 50 1.
84. 1, 38 ⊢ A ∈ power X, power_intro 83 50.
85. 1, 38 ⊢ app φ A = χ A X, map_from_term_app 8 7 84.
86. 1, 38 ⊢ χ A X = app φ A, eq_symm 85.
87. 1, 38 ⊢ f = app φ A, eq_trans 82 86.
88. 1, 38 ⊢ (A, f) ∈ φ, map_app_elim 9 84 87.
89. 1, 38 ⊢ f ∈ rng φ, rng_intro 88.
90. 1 ⊢ f ∈ Map X {∅, {∅}} → f ∈ rng φ, subj_intro 89.
91. 1 ⊢ ∀f. f ∈ Map X {∅, {∅}} → f ∈ rng φ, uq_intro 90.
92. 1 ⊢ Map X {∅, {∅}} ⊆ rng φ, incl_intro 91.
93. 1 ⊢ sur φ (power X) (Map X {∅, {∅}}), sur_intro 9 92.
94. 1 ⊢ bij φ (power X) (Map X {∅, {∅}}), bij_from_inj_sur 37 93.
95. 1 ⊢ ∃g. bij g (power X) (Map X {∅, {∅}}), ex_intro 94.
96. 1 ⊢ num_eq (power X) (Map X {∅, {∅}}), num_eq_intro 95.
power_equinum_indicators. ⊢ set X →
num_eq (power X) (Map X {∅, {∅}}), subj_intro 96.
Dependencies
The given proof depends on 12 axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, pairing, power, subset, substitution, union.