# Metamath Proof Explorer

## Theorem pw2eng

Description: The power set of a set is equinumerous to set exponentiation with a base of ordinal 2o . (Contributed by FL, 22-Feb-2011) (Revised by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion pw2eng ${⊢}{A}\in {V}\to 𝒫{A}\approx \left({{2}_{𝑜}}^{{A}}\right)$

### Proof

Step Hyp Ref Expression
1 pwexg ${⊢}{A}\in {V}\to 𝒫{A}\in \mathrm{V}$
2 ovexd ${⊢}{A}\in {V}\to {\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}\in \mathrm{V}$
3 id ${⊢}{A}\in {V}\to {A}\in {V}$
4 0ex ${⊢}\varnothing \in \mathrm{V}$
5 4 a1i ${⊢}{A}\in {V}\to \varnothing \in \mathrm{V}$
6 p0ex ${⊢}\left\{\varnothing \right\}\in \mathrm{V}$
7 6 a1i ${⊢}{A}\in {V}\to \left\{\varnothing \right\}\in \mathrm{V}$
8 0nep0 ${⊢}\varnothing \ne \left\{\varnothing \right\}$
9 8 a1i ${⊢}{A}\in {V}\to \varnothing \ne \left\{\varnothing \right\}$
10 eqid ${⊢}\left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},\left\{\varnothing \right\},\varnothing \right)\right)\right)=\left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},\left\{\varnothing \right\},\varnothing \right)\right)\right)$
11 3 5 7 9 10 pw2f1o ${⊢}{A}\in {V}\to \left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},\left\{\varnothing \right\},\varnothing \right)\right)\right):𝒫{A}\underset{1-1 onto}{⟶}{\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}$
12 f1oen2g ${⊢}\left(𝒫{A}\in \mathrm{V}\wedge {\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}\in \mathrm{V}\wedge \left({x}\in 𝒫{A}⟼\left({z}\in {A}⟼if\left({z}\in {x},\left\{\varnothing \right\},\varnothing \right)\right)\right):𝒫{A}\underset{1-1 onto}{⟶}{\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}\right)\to 𝒫{A}\approx \left({\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}\right)$
13 1 2 11 12 syl3anc ${⊢}{A}\in {V}\to 𝒫{A}\approx \left({\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}\right)$
14 df2o2 ${⊢}{2}_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$
15 14 oveq1i ${⊢}{{2}_{𝑜}}^{{A}}={\left\{\varnothing ,\left\{\varnothing \right\}\right\}}^{{A}}$
16 13 15 breqtrrdi ${⊢}{A}\in {V}\to 𝒫{A}\approx \left({{2}_{𝑜}}^{{A}}\right)$