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

Metamath Proof Explorer

Theorem pwen

Description: If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of TakeutiZaring p. 87. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion pwen ⊢ A ≈ B → 𝒫 A ≈ 𝒫 B

Proof

Step Hyp Ref Expression
1 relen ⊢ Rel ⁡ ≈
2 1 brrelex1i ⊢ A ≈ B → A ∈ V
3 pw2eng ⊢ A ∈ V → 𝒫 A ≈ 2 𝑜 A
4 2 3 syl ⊢ A ≈ B → 𝒫 A ≈ 2 𝑜 A
5 2onn ⊢ 2 𝑜 ∈ ω
6 5 elexi ⊢ 2 𝑜 ∈ V
7 6 enref ⊢ 2 𝑜 ≈ 2 𝑜
8 mapen ⊢ 2 𝑜 ≈ 2 𝑜 ∧ A ≈ B → 2 𝑜 A ≈ 2 𝑜 B
9 7 8 mpan ⊢ A ≈ B → 2 𝑜 A ≈ 2 𝑜 B
10 1 brrelex2i ⊢ A ≈ B → B ∈ V
11 pw2eng ⊢ B ∈ V → 𝒫 B ≈ 2 𝑜 B
12 ensym ⊢ 𝒫 B ≈ 2 𝑜 B → 2 𝑜 B ≈ 𝒫 B
13 10 11 12 3syl ⊢ A ≈ B → 2 𝑜 B ≈ 𝒫 B
14 entr ⊢ 2 𝑜 A ≈ 2 𝑜 B ∧ 2 𝑜 B ≈ 𝒫 B → 2 𝑜 A ≈ 𝒫 B
15 9 13 14 syl2anc ⊢ A ≈ B → 2 𝑜 A ≈ 𝒫 B
16 entr ⊢ 𝒫 A ≈ 2 𝑜 A ∧ 2 𝑜 A ≈ 𝒫 B → 𝒫 A ≈ 𝒫 B
17 4 15 16 syl2anc ⊢ A ≈ B → 𝒫 A ≈ 𝒫 B