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