# 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 ${⊢}{\phi }\to {A}\in {V}$
pw2f1o.2 ${⊢}{\phi }\to {B}\in {W}$
pw2f1o.3 ${⊢}{\phi }\to {C}\in {W}$
pw2f1o.4 ${⊢}{\phi }\to {B}\ne {C}$
pw2f1o.5 ${⊢}{F}=\left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\right)$
Assertion pw2f1o ${⊢}{\phi }\to {F}:𝒫{A}\underset{1-1 onto}{⟶}{\left\{{B},{C}\right\}}^{{A}}$

### Proof

Step Hyp Ref Expression
1 pw2f1o.1 ${⊢}{\phi }\to {A}\in {V}$
2 pw2f1o.2 ${⊢}{\phi }\to {B}\in {W}$
3 pw2f1o.3 ${⊢}{\phi }\to {C}\in {W}$
4 pw2f1o.4 ${⊢}{\phi }\to {B}\ne {C}$
5 pw2f1o.5 ${⊢}{F}=\left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\right)$
6 eqid ${⊢}\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)=\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)$
7 1 2 3 4 pw2f1olem ${⊢}{\phi }\to \left(\left({x}\in 𝒫{A}\wedge \left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)=\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\right)↔\left(\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\in \left({\left\{{B},{C}\right\}}^{{A}}\right)\wedge {x}={\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)}^{-1}\left[\left\{{C}\right\}\right]\right)\right)$
8 7 biimpa ${⊢}\left({\phi }\wedge \left({x}\in 𝒫{A}\wedge \left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)=\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\right)\right)\to \left(\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\in \left({\left\{{B},{C}\right\}}^{{A}}\right)\wedge {x}={\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)}^{-1}\left[\left\{{C}\right\}\right]\right)$
9 6 8 mpanr2 ${⊢}\left({\phi }\wedge {x}\in 𝒫{A}\right)\to \left(\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\in \left({\left\{{B},{C}\right\}}^{{A}}\right)\wedge {x}={\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)}^{-1}\left[\left\{{C}\right\}\right]\right)$
10 9 simpld ${⊢}\left({\phi }\wedge {x}\in 𝒫{A}\right)\to \left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\in \left({\left\{{B},{C}\right\}}^{{A}}\right)$
11 vex ${⊢}{y}\in \mathrm{V}$
12 11 cnvex ${⊢}{{y}}^{-1}\in \mathrm{V}$
13 12 imaex ${⊢}{{y}}^{-1}\left[\left\{{C}\right\}\right]\in \mathrm{V}$
14 13 a1i ${⊢}\left({\phi }\wedge {y}\in \left({\left\{{B},{C}\right\}}^{{A}}\right)\right)\to {{y}}^{-1}\left[\left\{{C}\right\}\right]\in \mathrm{V}$
15 1 2 3 4 pw2f1olem ${⊢}{\phi }\to \left(\left({x}\in 𝒫{A}\wedge {y}=\left({z}\in {A}⟼if\left({z}\in {x},{C},{B}\right)\right)\right)↔\left({y}\in \left({\left\{{B},{C}\right\}}^{{A}}\right)\wedge {x}={{y}}^{-1}\left[\left\{{C}\right\}\right]\right)\right)$
16 5 10 14 15 f1od ${⊢}{\phi }\to {F}:𝒫{A}\underset{1-1 onto}{⟶}{\left\{{B},{C}\right\}}^{{A}}$