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 φ A V
pw2f1o.2 φ B W
pw2f1o.3 φ C W
pw2f1o.4 φ B C
pw2f1o.5 F = x 𝒫 A z A if z x C B
Assertion pw2f1o φ F : 𝒫 A 1-1 onto B C A

Proof

Step Hyp Ref Expression
1 pw2f1o.1 φ A V
2 pw2f1o.2 φ B W
3 pw2f1o.3 φ C W
4 pw2f1o.4 φ B C
5 pw2f1o.5 F = x 𝒫 A z A if z x C B
6 eqid z A if z x C B = z A if z x C B
7 1 2 3 4 pw2f1olem φ x 𝒫 A z A if z x C B = z A if z x C B z A if z x C B B C A x = z A if z x C B -1 C
8 7 biimpa φ x 𝒫 A z A if z x C B = z A if z x C B z A if z x C B B C A x = z A if z x C B -1 C
9 6 8 mpanr2 φ x 𝒫 A z A if z x C B B C A x = z A if z x C B -1 C
10 9 simpld φ x 𝒫 A z A if z x C B B C A
11 vex y V
12 11 cnvex y -1 V
13 12 imaex y -1 C V
14 13 a1i φ y B C A y -1 C V
15 1 2 3 4 pw2f1olem φ x 𝒫 A y = z A if z x C B y B C A x = y -1 C
16 5 10 14 15 f1od φ F : 𝒫 A 1-1 onto B C A