Theorem pwen

Description: If two sets are equinumerous, then their power sets are equinumerous. Proposition 10.15 of TakeutiZaring p. 87. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Assertion	pwen	$$⊢A\approx B\to 𝒫A\approx 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		relen	$$⊢\mathrm{Rel}\approx$$
2	1	brrelex1i	$$⊢A\approx B\to A\in \mathrm{V}$$
3		pw2eng	$$⊢A\in \mathrm{V}\to 𝒫A\approx \left({2_{𝑜}}^A\right)$$
4	2 3	syl	$$⊢A\approx B\to 𝒫A\approx \left({2_{𝑜}}^A\right)$$
5		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
6	5	elexi	$$⊢2_{𝑜}\in \mathrm{V}$$
7	6	enref	$$⊢2_{𝑜}\approx 2_{𝑜}$$
8		mapen	$$⊢\left(2_{𝑜}\approx 2_{𝑜}\wedge A\approx B\right)\to \left({2_{𝑜}}^A\right)\approx \left({2_{𝑜}}^B\right)$$
9	7 8	mpan	$$⊢A\approx B\to \left({2_{𝑜}}^A\right)\approx \left({2_{𝑜}}^B\right)$$
10	1	brrelex2i	$$⊢A\approx B\to B\in \mathrm{V}$$
11		pw2eng	$$⊢B\in \mathrm{V}\to 𝒫B\approx \left({2_{𝑜}}^B\right)$$
12		ensym	$$⊢𝒫B\approx \left({2_{𝑜}}^B\right)\to \left({2_{𝑜}}^B\right)\approx 𝒫B$$
13	10 11 12	3syl	$$⊢A\approx B\to \left({2_{𝑜}}^B\right)\approx 𝒫B$$
14		entr	$$⊢\left(\left({2_{𝑜}}^A\right)\approx \left({2_{𝑜}}^B\right)\wedge \left({2_{𝑜}}^B\right)\approx 𝒫B\right)\to \left({2_{𝑜}}^A\right)\approx 𝒫B$$
15	9 13 14	syl2anc	$$⊢A\approx B\to \left({2_{𝑜}}^A\right)\approx 𝒫B$$
16		entr	$$⊢\left(𝒫A\approx \left({2_{𝑜}}^A\right)\wedge \left({2_{𝑜}}^A\right)\approx 𝒫B\right)\to 𝒫A\approx 𝒫B$$
17	4 15 16	syl2anc	$$⊢A\approx B\to 𝒫A\approx 𝒫B$$