Theorem enmappw

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

	Ref	Expression
Assertion	enmappw	$$⊢\left(A\in V\wedge B\in W\right)\to \left({𝒫B}^A\right)\approx \left({𝒫A}^B\right)$$

Proof

Step	Hyp	Ref	Expression
1		enrelmap	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(A\times B\right)\approx \left({𝒫B}^A\right)$$
2	1	ensymd	$$⊢\left(A\in V\wedge B\in W\right)\to \left({𝒫B}^A\right)\approx 𝒫\left(A\times B\right)$$
3		enrelmapr	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(A\times B\right)\approx \left({𝒫A}^B\right)$$
4		entr	$$⊢\left(\left({𝒫B}^A\right)\approx 𝒫\left(A\times B\right)\wedge 𝒫\left(A\times B\right)\approx \left({𝒫A}^B\right)\right)\to \left({𝒫B}^A\right)\approx \left({𝒫A}^B\right)$$
5	2 3 4	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to \left({𝒫B}^A\right)\approx \left({𝒫A}^B\right)$$