Metamath Proof Explorer


Theorem enmappwid

Description: The set of all mappings from the powerset to the powerset is equinumerous to the set of all mappings from the set to the powerset of the powerset. (Contributed by RP, 27-Apr-2021)

Ref Expression
Assertion enmappwid ( 𝐴𝑉 → ( 𝒫 𝐴m 𝒫 𝐴 ) ≈ ( 𝒫 𝒫 𝐴m 𝐴 ) )

Proof

Step Hyp Ref Expression
1 pwexg ( 𝐴𝑉 → 𝒫 𝐴 ∈ V )
2 enmappw ( ( 𝒫 𝐴 ∈ V ∧ 𝐴𝑉 ) → ( 𝒫 𝐴m 𝒫 𝐴 ) ≈ ( 𝒫 𝒫 𝐴m 𝐴 ) )
3 1 2 mpancom ( 𝐴𝑉 → ( 𝒫 𝐴m 𝒫 𝐴 ) ≈ ( 𝒫 𝒫 𝐴m 𝐴 ) )