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	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pwexg	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
2		ovexd	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ , { ∅ } } ↑m 𝐴 ) ∈ V )
3		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
4		0ex	⊢ ∅ ∈ V
5	4	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∅ ∈ V )
6		p0ex	⊢ { ∅ } ∈ V
7	6	a1i	⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ∈ V )
8		0nep0	⊢ ∅ ≠ { ∅ }
9	8	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∅ ≠ { ∅ } )
10		eqid	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , { ∅ } , ∅ ) ) ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , { ∅ } , ∅ ) ) )
11	3 5 7 9 10	pw2f1o	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , { ∅ } , ∅ ) ) ) : 𝒫 𝐴 –1-1-onto→ ( { ∅ , { ∅ } } ↑m 𝐴 ) )
12		f1oen2g	⊢ ( ( 𝒫 𝐴 ∈ V ∧ ( { ∅ , { ∅ } } ↑m 𝐴 ) ∈ V ∧ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝑧 ∈ 𝐴 ↦ if ( 𝑧 ∈ 𝑥 , { ∅ } , ∅ ) ) ) : 𝒫 𝐴 –1-1-onto→ ( { ∅ , { ∅ } } ↑m 𝐴 ) ) → 𝒫 𝐴 ≈ ( { ∅ , { ∅ } } ↑m 𝐴 ) )
13	1 2 11 12	syl3anc	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ ( { ∅ , { ∅ } } ↑m 𝐴 ) )
14		df2o2	⊢ 2o = { ∅ , { ∅ } }
15	14	oveq1i	⊢ ( 2o ↑m 𝐴 ) = ( { ∅ , { ∅ } } ↑m 𝐴 )
16	13 15	breqtrrdi	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ≈ ( 2o ↑m 𝐴 ) )