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 ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵 )

Proof

Step Hyp Ref Expression
1 relen ⊢ Rel ≈
2 1 brrelex1i ⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
3 pw2eng ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
4 2 3 syl ⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
5 2onn ⊢ 2o ∈ ω
6 5 elexi ⊢ 2o ∈ V
7 6 enref ⊢ 2o ≈ 2o
8 mapen ⊢ ( ( 2o ≈ 2o ∧ 𝐴 ≈ 𝐵 ) → ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) )
9 7 8 mpan ⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) )
10 1 brrelex2i ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
11 pw2eng ⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
12 ensym ⊢ ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
13 10 11 12 3syl ⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
14 entr ⊢ ( ( ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 )
15 9 13 14 syl2anc ⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 )
16 entr ⊢ ( ( 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) ∧ ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 ) → 𝒫 𝐴 ≈ 𝒫 𝐵 )
17 4 15 16 syl2anc ⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵 )