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

Metamath Proof Explorer

Theorem pw2f1o

Description: The power set of a set is equinumerous to set exponentiation with an unordered pair base of ordinal 2. Generalized from Proposition 10.44 of TakeutiZaring p. 96. (Contributed by Mario Carneiro, 6-Oct-2014)

Ref Expression
Hypotheses pw2f1o.1 
|- ( ph -> A e. V )
pw2f1o.2 
|- ( ph -> B e. W )
pw2f1o.3 
|- ( ph -> C e. W )
pw2f1o.4 
|- ( ph -> B =/= C )
pw2f1o.5 
|- F = ( x e. ~P A |-> ( z e. A |-> if ( z e. x , C , B ) ) )
Assertion pw2f1o 
|- ( ph -> F : ~P A -1-1-onto-> ( { B , C } ^m A ) )

Proof

Step Hyp Ref Expression
1 pw2f1o.1 
 |-  ( ph -> A e. V )
2 pw2f1o.2 
 |-  ( ph -> B e. W )
3 pw2f1o.3 
 |-  ( ph -> C e. W )
4 pw2f1o.4 
 |-  ( ph -> B =/= C )
5 pw2f1o.5 
 |-  F = ( x e. ~P A |-> ( z e. A |-> if ( z e. x , C , B ) ) )
6 eqid 
 |-  ( z e. A |-> if ( z e. x , C , B ) ) = ( z e. A |-> if ( z e. x , C , B ) )
7 1 2 3 4 pw2f1olem 
 |-  ( ph -> ( ( x e. ~P A /\ ( z e. A |-> if ( z e. x , C , B ) ) = ( z e. A |-> if ( z e. x , C , B ) ) ) <-> ( ( z e. A |-> if ( z e. x , C , B ) ) e. ( { B , C } ^m A ) /\ x = ( `' ( z e. A |-> if ( z e. x , C , B ) ) " { C } ) ) ) )
8 7 biimpa 
 |-  ( ( ph /\ ( x e. ~P A /\ ( z e. A |-> if ( z e. x , C , B ) ) = ( z e. A |-> if ( z e. x , C , B ) ) ) ) -> ( ( z e. A |-> if ( z e. x , C , B ) ) e. ( { B , C } ^m A ) /\ x = ( `' ( z e. A |-> if ( z e. x , C , B ) ) " { C } ) ) )
9 6 8 mpanr2 
 |-  ( ( ph /\ x e. ~P A ) -> ( ( z e. A |-> if ( z e. x , C , B ) ) e. ( { B , C } ^m A ) /\ x = ( `' ( z e. A |-> if ( z e. x , C , B ) ) " { C } ) ) )
10 9 simpld 
 |-  ( ( ph /\ x e. ~P A ) -> ( z e. A |-> if ( z e. x , C , B ) ) e. ( { B , C } ^m A ) )
11 vex 
 |-  y e. _V
12 11 cnvex 
 |-  `' y e. _V
13 12 imaex 
 |-  ( `' y " { C } ) e. _V
14 13 a1i 
 |-  ( ( ph /\ y e. ( { B , C } ^m A ) ) -> ( `' y " { C } ) e. _V )
15 1 2 3 4 pw2f1olem 
 |-  ( ph -> ( ( x e. ~P A /\ y = ( z e. A |-> if ( z e. x , C , B ) ) ) <-> ( y e. ( { B , C } ^m A ) /\ x = ( `' y " { C } ) ) ) )
16 5 10 14 15 f1od 
 |-  ( ph -> F : ~P A -1-1-onto-> ( { B , C } ^m A ) )