# 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 -> ~P A ~~ ~P B )`

### Proof

Step Hyp Ref Expression
1 relen
` |-  Rel ~~`
2 1 brrelex1i
` |-  ( A ~~ B -> A e. _V )`
3 pw2eng
` |-  ( A e. _V -> ~P A ~~ ( 2o ^m A ) )`
4 2 3 syl
` |-  ( A ~~ B -> ~P A ~~ ( 2o ^m A ) )`
5 2onn
` |-  2o e. _om`
6 5 elexi
` |-  2o e. _V`
7 6 enref
` |-  2o ~~ 2o`
8 mapen
` |-  ( ( 2o ~~ 2o /\ A ~~ B ) -> ( 2o ^m A ) ~~ ( 2o ^m B ) )`
9 7 8 mpan
` |-  ( A ~~ B -> ( 2o ^m A ) ~~ ( 2o ^m B ) )`
10 1 brrelex2i
` |-  ( A ~~ B -> B e. _V )`
11 pw2eng
` |-  ( B e. _V -> ~P B ~~ ( 2o ^m B ) )`
12 ensym
` |-  ( ~P B ~~ ( 2o ^m B ) -> ( 2o ^m B ) ~~ ~P B )`
13 10 11 12 3syl
` |-  ( A ~~ B -> ( 2o ^m B ) ~~ ~P B )`
14 entr
` |-  ( ( ( 2o ^m A ) ~~ ( 2o ^m B ) /\ ( 2o ^m B ) ~~ ~P B ) -> ( 2o ^m A ) ~~ ~P B )`
15 9 13 14 syl2anc
` |-  ( A ~~ B -> ( 2o ^m A ) ~~ ~P B )`
16 entr
` |-  ( ( ~P A ~~ ( 2o ^m A ) /\ ( 2o ^m A ) ~~ ~P B ) -> ~P A ~~ ~P B )`
17 4 15 16 syl2anc
` |-  ( A ~~ B -> ~P A ~~ ~P B )`