Proof
001. 1 ⊢ set X, hypo.
002. 2 ⊢ φ = {t | ∃A. A ∈ power X ∧ t = (A, χ A X)}, hypo.
003. 3 ⊢ A ∈ power X, hypo.
004. 3 ⊢ A ⊆ X, power_elim 3.
005. 3 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 4.
006. 1, 3 ⊢ χ A X ∈ Map X {∅, {∅}}, Map_intro 5 1.
007. 1 ⊢ A ∈ power X → χ A X ∈ Map X {∅, {∅}}, subj_intro 6.
008. 1 ⊢ ∀A. A ∈ power X → χ A X ∈ Map X {∅, {∅}}, uq_intro 7.
009. 1, 2 ⊢ map φ (power X) (Map X {∅, {∅}}), map_from_term 2 8.
010. 10 ⊢ A ∈ power X, hypo.
011. 11 ⊢ B ∈ power X, hypo.
012. 12 ⊢ app φ A = app φ B, hypo.
013. 1, 2, 10 ⊢ app φ A = χ A X, map_from_term_app 2 8 10.
014. 1, 2, 11 ⊢ app φ B = χ B X, map_from_term_app 2 8 11.
015. 1, 2, 10, 12 ⊢ χ A X = app φ B, eq_symm_trans 13 12.
016. 1, 2, 10, 11, 12 ⊢ χ A X = χ B X, eq_trans 15 14.
017. 10 ⊢ A ⊆ X, power_elim 10.
018. 11 ⊢ B ⊆ X, power_elim 11.
019. 19 ⊢ x ∈ A, hypo.
020. 10, 19 ⊢ app (χ A X) x = {∅}, indicator_app_is_one 17 19.
021. 1, 2, 10, 11, 12, 19 ⊢ app (χ B X) x = {∅},
eq_subst 16 20, P t ↔ app t x = {∅}.
022. 10, 19 ⊢ x ∈ X, incl_elim 17 19.
023. 1, 2, 10, 11, 12, 19 ⊢ x ∈ B, from_indicator_app_is_one 18 22 21.
024. 1, 2, 10, 11, 12 ⊢ x ∈ A → x ∈ B, subj_intro 23.
025. 25 ⊢ x ∈ B, hypo.
026. 11, 25 ⊢ app (χ B X) x = {∅}, indicator_app_is_one 18 25.
027. 1, 2, 10, 11, 12, 25 ⊢ app (χ A X) x = {∅},
eq_subst_rev 16 26, P t ↔ app t x = {∅}.
028. 11, 25 ⊢ x ∈ X, incl_elim 18 25.
029. 1, 2, 10, 11, 12, 25 ⊢ x ∈ A, from_indicator_app_is_one 17 28 27.
030. 1, 2, 10, 11, 12 ⊢ x ∈ B → x ∈ A, subj_intro 29.
031. 1, 2, 10, 11, 12 ⊢ x ∈ A ↔ x ∈ B, bij_intro 24 30.
032. 1, 2, 10, 11, 12 ⊢ ∀x. x ∈ A ↔ x ∈ B, uq_intro 31.
033. 1, 2, 10, 11, 12 ⊢ A = B, ext 32.
034. 1, 2 ⊢ A ∈ power X → B ∈ power X → app φ A = app φ B → A = B,
subj_intro_iii 33.
035. 1, 2 ⊢ ∀B. A ∈ power X → B ∈ power X →
app φ A = app φ B → A = B, uq_intro 34.
036. 1, 2 ⊢ ∀A. ∀B. A ∈ power X → B ∈ power X →
app φ A = app φ B → A = B, uq_intro 35.
037. 1, 2 ⊢ inj φ (power X) (Map X {∅, {∅}}), inj_intro 9 36.
038. 38 ⊢ f ∈ Map X {∅, {∅}}, hypo.
039. 38 ⊢ map f X {∅, {∅}}, Map_elim 38.
040. 38 ⊢ function f ∧ dom f = X ∧ rng f ⊆ {∅, {∅}}, map_unfold 39.
041. 38 ⊢ dom f = X, conj_elimlr 40.
042. 42 ⊢ A = inv_img f {{∅}}, hypo.
043. 43 ⊢ x ∈ X, hypo.
044. 38, 43 ⊢ app f x ∈ {∅, {∅}}, map_app_in_cod 39 43.
045. 38, 43 ⊢ app f x ∈ {∅} ∨ app f x ∈ {{∅}}, union_elim 44.
046. 46 ⊢ app f x ∈ {∅}, hypo.
047. 46 ⊢ app f x = ∅, sg_elim empty_set_is_set 46.
048. 46 ⊢ ∅ = app f x, eq_symm 47.
049. 38, 43, 46 ⊢ (x, ∅) ∈ f, map_app_elim 39 43 48.
050. ⊢ inv_img f {{∅}} ⊆ dom f, inv_img_incl_in_dom.
051. 42 ⊢ A ⊆ dom f, eq_subst_rev 42 50, P t ↔ t ⊆ dom f.
052. 38, 42 ⊢ A ⊆ X, eq_subst 41 51, P t ↔ A ⊆ t.
053. 53 ⊢ x ∈ A, hypo.
054. 42, 53 ⊢ x ∈ inv_img f {{∅}}, eq_subst 42 53.
055. 42, 53 ⊢ ∃y. y ∈ {{∅}} ∧ (x, y) ∈ f, inv_img_elim 54.
056. 56 ⊢ y ∈ {{∅}} ∧ (x, y) ∈ f, hypo.
057. 56 ⊢ y ∈ {{∅}}, conj_eliml 56.
058. 56 ⊢ (x, y) ∈ f, conj_elimr 56.
059. 38 ⊢ function f, conj_elimll 40.
060. 38, 43, 46, 56 ⊢ y = ∅, fn_unique_value 59 58 49.
061. ⊢ set {∅}, set_sg empty_set_is_set.
062. 56 ⊢ y = {∅}, sg_elim 61 57.
063. 38, 43, 46, 56 ⊢ ∅ = {∅}, eq_symm_trans 60 62.
064. 38, 43, 46, 56 ⊢ ⊥, neg_elim zero_neq_one 63.
065. 38, 42, 43, 46, 53 ⊢ ⊥, ex_elim 55 64.
066. 38, 42, 43, 46 ⊢ ¬x ∈ A, neg_intro 65.
067. 38, 42, 43, 46 ⊢ x ∈ X \ A, diff_intro 43 66.
068. 38, 42, 43, 46 ⊢ app (χ A X) x = ∅, indicator_app_is_zero 52 67.
069. 38, 42, 43, 46 ⊢ ∅ = app (χ A X) x, eq_symm 68.
070. 38, 42, 43, 46 ⊢ app f x = app (χ A X) x, eq_trans 47 69.
071. 71 ⊢ app f x ∈ {{∅}}, hypo.
072. 71 ⊢ app f x = {∅}, sg_elim 61 71.
073. 71 ⊢ {∅} = app f x, eq_symm 72.
074. 38, 43, 71 ⊢ (x, {∅}) ∈ f, map_app_elim 39 43 73.
075. ⊢ {∅} = {∅}, eq_refl.
076. ⊢ {∅} ∈ {{∅}}, sg_intro 61 75.
077. 38, 43, 71 ⊢ x ∈ inv_img f {{∅}}, inv_img_intro 76 74.
078. 38, 42, 43, 71 ⊢ x ∈ A, eq_subst_rev 42 77, P t ↔ x ∈ t.
079. 38, 42, 43, 71 ⊢ app (χ A X) x = {∅}, indicator_app_is_one 52 78.
080. 38, 42, 43, 71 ⊢ {∅} = app (χ A X) x, eq_symm 79.
081. 38, 42, 43, 71 ⊢ app f x = app (χ A X) x, eq_trans 72 80.
082. 38, 42, 43 ⊢ app f x = app (χ A X) x, disj_elim 45 70 81.
083. 38, 42 ⊢ x ∈ X → app f x = app (χ A X) x, subj_intro 82.
084. 38, 42 ⊢ ∀x. x ∈ X → app f x = app (χ A X) x, uq_intro 83.
085. 38, 42 ⊢ map (χ A X) X {∅, {∅}}, indicator_is_map 52.
086. 38, 42 ⊢ f = χ A X, map_extensionality 39 85 84.
087. 1, 38, 42 ⊢ set A, subset 52 1.
088. 1, 38, 42 ⊢ A ∈ power X, power_intro 87 52.
089. 1, 2, 38, 42 ⊢ app φ A = χ A X, map_from_term_app 2 8 88.
090. 1, 2, 38, 42 ⊢ χ A X = app φ A, eq_symm 89.
091. 1, 2, 38, 42 ⊢ f = app φ A, eq_trans 86 90.
092. 1, 2, 38, 42 ⊢ (A, f) ∈ φ, map_app_elim 9 88 91.
093. 1, 2, 38, 42 ⊢ f ∈ rng φ, rng_intro 92.
094. 1, 2, 38 ⊢ A = inv_img f {{∅}} → f ∈ rng φ, subj_intro 93.
095. 1, 2, 38 ⊢ ∀A. A = inv_img f {{∅}} → f ∈ rng φ, uq_intro 94.
096. 1, 2, 38 ⊢ f ∈ rng φ, disused_eq 95.
097. 1, 2 ⊢ f ∈ Map X {∅, {∅}} → f ∈ rng φ, subj_intro 96.
098. 1, 2 ⊢ ∀f. f ∈ Map X {∅, {∅}} → f ∈ rng φ, uq_intro 97.
099. 1, 2 ⊢ Map X {∅, {∅}} ⊆ rng φ, incl_intro 98.
100. 1, 2 ⊢ sur φ (power X) (Map X {∅, {∅}}), sur_intro 9 99.
101. 1, 2 ⊢ bij φ (power X) (Map X {∅, {∅}}), bij_from_inj_sur 37 100.
102. 1, 2 ⊢ ∃φ. bij φ (power X) (Map X {∅, {∅}}), ex_intro 101.
103. 1 ⊢ φ = {t | ∃A. A ∈ power X ∧ t = (A, χ A X)} →
∃φ. bij φ (power X) (Map X {∅, {∅}}), subj_intro 102.
104. 1 ⊢ ∀φ. φ = {t | ∃A. A ∈ power X ∧ t = (A, χ A X)} →
∃φ. bij φ (power X) (Map X {∅, {∅}}), uq_intro 103.
105. 1 ⊢ ∃φ. bij φ (power X) (Map X {∅, {∅}}), disused_eq 104.
106. 1 ⊢ num_eq (power X) (Map X {∅, {∅}}), num_eq_intro 105.
power_equinum_indicators. ⊢ set X →
num_eq (power X) (Map X {∅, {∅}}), subj_intro 106.
Dependencies
The given proof depends on 12 axioms:
comp, efq, eq_refl, eq_subst, ext, infinity, lem, pairing, power, subset, substitution, union.