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

Metamath Proof Explorer

Theorem pw2eng

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2o . (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion pw2eng 
|- ( A e. V -> ~P A ~~ ( 2o ^m A ) )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. V -> ~P A e. _V )
2 ovexd 
 |-  ( A e. V -> ( { (/) , { (/) } } ^m A ) e. _V )
3 id 
 |-  ( A e. V -> A e. V )
4 0ex 
 |-  (/) e. _V
5 4 a1i 
 |-  ( A e. V -> (/) e. _V )
6 p0ex 
 |-  { (/) } e. _V
7 6 a1i 
 |-  ( A e. V -> { (/) } e. _V )
8 0nep0 
 |-  (/) =/= { (/) }
9 8 a1i 
 |-  ( A e. V -> (/) =/= { (/) } )
10 eqid 
 |-  ( x e. ~P A |-> ( z e. A |-> if ( z e. x , { (/) } , (/) ) ) ) = ( x e. ~P A |-> ( z e. A |-> if ( z e. x , { (/) } , (/) ) ) )
11 3 5 7 9 10 pw2f1o 
 |-  ( A e. V -> ( x e. ~P A |-> ( z e. A |-> if ( z e. x , { (/) } , (/) ) ) ) : ~P A -1-1-onto-> ( { (/) , { (/) } } ^m A ) )
12 f1oen2g 
 |-  ( ( ~P A e. _V /\ ( { (/) , { (/) } } ^m A ) e. _V /\ ( x e. ~P A |-> ( z e. A |-> if ( z e. x , { (/) } , (/) ) ) ) : ~P A -1-1-onto-> ( { (/) , { (/) } } ^m A ) ) -> ~P A ~~ ( { (/) , { (/) } } ^m A ) )
13 1 2 11 12 syl3anc 
 |-  ( A e. V -> ~P A ~~ ( { (/) , { (/) } } ^m A ) )
14 df2o2 
 |-  2o = { (/) , { (/) } }
15 14 oveq1i 
 |-  ( 2o ^m A ) = ( { (/) , { (/) } } ^m A )
16 13 15 breqtrrdi 
 |-  ( A e. V -> ~P A ~~ ( 2o ^m A ) )