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}\approx {B}\to 𝒫{A}\approx 𝒫{B}$

Proof

Step Hyp Ref Expression
1 relen ${⊢}\mathrm{Rel}\approx$
2 1 brrelex1i ${⊢}{A}\approx {B}\to {A}\in \mathrm{V}$
3 pw2eng ${⊢}{A}\in \mathrm{V}\to 𝒫{A}\approx \left({{2}_{𝑜}}^{{A}}\right)$
4 2 3 syl ${⊢}{A}\approx {B}\to 𝒫{A}\approx \left({{2}_{𝑜}}^{{A}}\right)$
5 2onn ${⊢}{2}_{𝑜}\in \mathrm{\omega }$
6 5 elexi ${⊢}{2}_{𝑜}\in \mathrm{V}$
7 6 enref ${⊢}{2}_{𝑜}\approx {2}_{𝑜}$
8 mapen ${⊢}\left({2}_{𝑜}\approx {2}_{𝑜}\wedge {A}\approx {B}\right)\to \left({{2}_{𝑜}}^{{A}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
9 7 8 mpan ${⊢}{A}\approx {B}\to \left({{2}_{𝑜}}^{{A}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)$
10 1 brrelex2i ${⊢}{A}\approx {B}\to {B}\in \mathrm{V}$
11 pw2eng ${⊢}{B}\in \mathrm{V}\to 𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)$
12 ensym ${⊢}𝒫{B}\approx \left({{2}_{𝑜}}^{{B}}\right)\to \left({{2}_{𝑜}}^{{B}}\right)\approx 𝒫{B}$
13 10 11 12 3syl ${⊢}{A}\approx {B}\to \left({{2}_{𝑜}}^{{B}}\right)\approx 𝒫{B}$
14 entr ${⊢}\left(\left({{2}_{𝑜}}^{{A}}\right)\approx \left({{2}_{𝑜}}^{{B}}\right)\wedge \left({{2}_{𝑜}}^{{B}}\right)\approx 𝒫{B}\right)\to \left({{2}_{𝑜}}^{{A}}\right)\approx 𝒫{B}$
15 9 13 14 syl2anc ${⊢}{A}\approx {B}\to \left({{2}_{𝑜}}^{{A}}\right)\approx 𝒫{B}$
16 entr ${⊢}\left(𝒫{A}\approx \left({{2}_{𝑜}}^{{A}}\right)\wedge \left({{2}_{𝑜}}^{{A}}\right)\approx 𝒫{B}\right)\to 𝒫{A}\approx 𝒫{B}$
17 4 15 16 syl2anc ${⊢}{A}\approx {B}\to 𝒫{A}\approx 𝒫{B}$