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	⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2	1	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
3		pw2eng	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
4	2 3	syl	⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )
5		2onn	⊢ 2o ∈ ω
6	5	elexi	⊢ 2o ∈ V
7	6	enref	⊢ 2o ≈ 2o
8		mapen	⊢ ( ( 2o ≈ 2o ∧ 𝐴 ≈ 𝐵 ) → ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) )
9	7 8	mpan	⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) )
10	1	brrelex2i	⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
11		pw2eng	⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
12		ensym	⊢ ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
13	10 11 12	3syl	⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 )
14		entr	⊢ ( ( ( 2o ↑m 𝐴 ) ≈ ( 2o ↑m 𝐵 ) ∧ ( 2o ↑m 𝐵 ) ≈ 𝒫 𝐵 ) → ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 )
15	9 13 14	syl2anc	⊢ ( 𝐴 ≈ 𝐵 → ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 )
16		entr	⊢ ( ( 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) ∧ ( 2o ↑m 𝐴 ) ≈ 𝒫 𝐵 ) → 𝒫 𝐴 ≈ 𝒫 𝐵 )
17	4 15 16	syl2anc	⊢ ( 𝐴 ≈ 𝐵 → 𝒫 𝐴 ≈ 𝒫 𝐵 )