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