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 φAV
pw2f1o.2 φBW
pw2f1o.3 φCW
pw2f1o.4 φBC
pw2f1o.5 F=x𝒫AzAifzxCB
Assertion pw2f1o φF:𝒫A1-1 ontoBCA

Proof

Step Hyp Ref Expression
1 pw2f1o.1 φAV
2 pw2f1o.2 φBW
3 pw2f1o.3 φCW
4 pw2f1o.4 φBC
5 pw2f1o.5 F=x𝒫AzAifzxCB
6 eqid zAifzxCB=zAifzxCB
7 1 2 3 4 pw2f1olem φx𝒫AzAifzxCB=zAifzxCBzAifzxCBBCAx=zAifzxCB-1C
8 7 biimpa φx𝒫AzAifzxCB=zAifzxCBzAifzxCBBCAx=zAifzxCB-1C
9 6 8 mpanr2 φx𝒫AzAifzxCBBCAx=zAifzxCB-1C
10 9 simpld φx𝒫AzAifzxCBBCA
11 vex yV
12 11 cnvex y-1V
13 12 imaex y-1CV
14 13 a1i φyBCAy-1CV
15 1 2 3 4 pw2f1olem φx𝒫Ay=zAifzxCByBCAx=y-1C
16 5 10 14 15 f1od φF:𝒫A1-1 ontoBCA