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 -> ~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 )