This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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