This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pw2eng

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2o . (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion pw2eng ⊢ A ∈ V → 𝒫 A ≈ 2 𝑜 A

Proof

Step Hyp Ref Expression
1 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
2 ovexd ⊢ A ∈ V → ∅ ∅ A ∈ V
3 id ⊢ A ∈ V → A ∈ V
4 0ex ⊢ ∅ ∈ V
5 4 a1i ⊢ A ∈ V → ∅ ∈ V
6 p0ex ⊢ ∅ ∈ V
7 6 a1i ⊢ A ∈ V → ∅ ∈ V
8 0nep0 ⊢ ∅ ≠ ∅
9 8 a1i ⊢ A ∈ V → ∅ ≠ ∅
10 eqid ⊢ x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x ∅ ∅ = x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x ∅ ∅
11 3 5 7 9 10 pw2f1o ⊢ A ∈ V → x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x ∅ ∅ : 𝒫 A ⟶ 1-1 onto ∅ ∅ A
12 f1oen2g ⊢ 𝒫 A ∈ V ∧ ∅ ∅ A ∈ V ∧ x ∈ 𝒫 A ⟼ z ∈ A ⟼ if z ∈ x ∅ ∅ : 𝒫 A ⟶ 1-1 onto ∅ ∅ A → 𝒫 A ≈ ∅ ∅ A
13 1 2 11 12 syl3anc ⊢ A ∈ V → 𝒫 A ≈ ∅ ∅ A
14 df2o2 ⊢ 2 𝑜 = ∅ ∅
15 14 oveq1i ⊢ 2 𝑜 A = ∅ ∅ A
16 13 15 breqtrrdi ⊢ A ∈ V → 𝒫 A ≈ 2 𝑜 A