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	$$⊢A\in V\to \left({𝒫A}^{𝒫A}\right)\approx \left({𝒫𝒫A}^A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$$⊢A\in V\to 𝒫A\in \mathrm{V}$$
2		enmappw	$$⊢\left(𝒫A\in \mathrm{V}\wedge A\in V\right)\to \left({𝒫A}^{𝒫A}\right)\approx \left({𝒫𝒫A}^A\right)$$
3	1 2	mpancom	$$⊢A\in V\to \left({𝒫A}^{𝒫A}\right)\approx \left({𝒫𝒫A}^A\right)$$