Theorem hashpw

Description: The size of the power set of a finite set is 2 raised to the power of the size of the set. (Contributed by Paul Chapman, 30-Nov-2012) (Proof shortened by Mario Carneiro, 5-Aug-2014)

	Ref	Expression
Assertion	hashpw	$$⊢A\in \mathrm{Fin}\to \left|𝒫A\right|=2^{\left|A\right|}$$

Proof

Step	Hyp	Ref	Expression
1		pweq	$$⊢x=A\to 𝒫x=𝒫A$$
2	1	fveq2d	$$⊢x=A\to \left|𝒫x\right|=\left|𝒫A\right|$$
3		fveq2	$$⊢x=A\to \left|x\right|=\left|A\right|$$
4	3	oveq2d	$$⊢x=A\to 2^{\left|x\right|}=2^{\left|A\right|}$$
5	2 4	eqeq12d	$$⊢x=A\to \left(\left|𝒫x\right|=2^{\left|x\right|}\leftrightarrow \left|𝒫A\right|=2^{\left|A\right|}\right)$$
6		vex	$$⊢x\in \mathrm{V}$$
7	6	pw2en	$$⊢𝒫x\approx \left({2_{𝑜}}^x\right)$$
8		pwfi	$$⊢x\in \mathrm{Fin}\leftrightarrow 𝒫x\in \mathrm{Fin}$$
9	8	biimpi	$$⊢x\in \mathrm{Fin}\to 𝒫x\in \mathrm{Fin}$$
10		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
11		prfi	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}\in \mathrm{Fin}$$
12	10 11	eqeltri	$$⊢2_{𝑜}\in \mathrm{Fin}$$
13		mapfi	$$⊢\left(2_{𝑜}\in \mathrm{Fin}\wedge x\in \mathrm{Fin}\right)\to {2_{𝑜}}^x\in \mathrm{Fin}$$
14	12 13	mpan	$$⊢x\in \mathrm{Fin}\to {2_{𝑜}}^x\in \mathrm{Fin}$$
15		hashen	$$⊢\left(𝒫x\in \mathrm{Fin}\wedge {2_{𝑜}}^x\in \mathrm{Fin}\right)\to \left(\left|𝒫x\right|=\left|{2_{𝑜}}^x\right|\leftrightarrow 𝒫x\approx \left({2_{𝑜}}^x\right)\right)$$
16	9 14 15	syl2anc	$$⊢x\in \mathrm{Fin}\to \left(\left|𝒫x\right|=\left|{2_{𝑜}}^x\right|\leftrightarrow 𝒫x\approx \left({2_{𝑜}}^x\right)\right)$$
17	7 16	mpbiri	$$⊢x\in \mathrm{Fin}\to \left|𝒫x\right|=\left|{2_{𝑜}}^x\right|$$
18		hashmap	$$⊢\left(2_{𝑜}\in \mathrm{Fin}\wedge x\in \mathrm{Fin}\right)\to \left|{2_{𝑜}}^x\right|={\left|2_{𝑜}\right|}^{\left|x\right|}$$
19	12 18	mpan	$$⊢x\in \mathrm{Fin}\to \left|{2_{𝑜}}^x\right|={\left|2_{𝑜}\right|}^{\left|x\right|}$$
20		hash2	$$⊢\left|2_{𝑜}\right|=2$$
21	20	oveq1i	$$⊢{\left|2_{𝑜}\right|}^{\left|x\right|}=2^{\left|x\right|}$$
22	19 21	eqtrdi	$$⊢x\in \mathrm{Fin}\to \left|{2_{𝑜}}^x\right|=2^{\left|x\right|}$$
23	17 22	eqtrd	$$⊢x\in \mathrm{Fin}\to \left|𝒫x\right|=2^{\left|x\right|}$$
24	5 23	vtoclga	$$⊢A\in \mathrm{Fin}\to \left|𝒫A\right|=2^{\left|A\right|}$$