Theorem enrelmapr

Description: The set of all possible relations between two sets is equinumerous to the set of all mappings from one set to the powerset of the other. (Contributed by RP, 27-Apr-2021)

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

Proof

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