Theorem enrelmap

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. See rfovf1od for a demonstration of a natural one-to-one onto mapping. (Contributed by RP, 27-Apr-2021)

	Ref	Expression
Assertion	enrelmap	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(A\times B\right)\approx \left({𝒫B}^A\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		xpexg	$$⊢\left(B\in W\wedge A\in V\right)\to B\times A\in \mathrm{V}$$
5	4	ancoms	$$⊢\left(A\in V\wedge B\in W\right)\to B\times A\in \mathrm{V}$$
6		pw2eng	$$⊢B\times A\in \mathrm{V}\to 𝒫\left(B\times A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
7	5 6	syl	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(B\times A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
8		entr	$$⊢\left(𝒫\left(A\times B\right)\approx 𝒫\left(B\times A\right)\wedge 𝒫\left(B\times A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)\right)\to 𝒫\left(A\times B\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
9	3 7 8	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(A\times B\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
10		pw2eng	$$⊢B\in W\to 𝒫B\approx \left({2_{𝑜}}^B\right)$$
11		enrefg	$$⊢A\in V\to A\approx A$$
12		mapen	$$⊢\left(𝒫B\approx \left({2_{𝑜}}^B\right)\wedge A\approx A\right)\to \left({𝒫B}^A\right)\approx \left({\left({2_{𝑜}}^B\right)}^A\right)$$
13	10 11 12	syl2anr	$$⊢\left(A\in V\wedge B\in W\right)\to \left({𝒫B}^A\right)\approx \left({\left({2_{𝑜}}^B\right)}^A\right)$$
14		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
15		simpr	$$⊢\left(A\in V\wedge B\in W\right)\to B\in W$$
16		simpl	$$⊢\left(A\in V\wedge B\in W\right)\to A\in V$$
17		mapxpen	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge B\in W\wedge A\in V\right)\to \left({\left({2_{𝑜}}^B\right)}^A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
18	14 15 16 17	mp3an2i	$$⊢\left(A\in V\wedge B\in W\right)\to \left({\left({2_{𝑜}}^B\right)}^A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
19		entr	$$⊢\left(\left({𝒫B}^A\right)\approx \left({\left({2_{𝑜}}^B\right)}^A\right)\wedge \left({\left({2_{𝑜}}^B\right)}^A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)\right)\to \left({𝒫B}^A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
20	13 18 19	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to \left({𝒫B}^A\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)$$
21	20	ensymd	$$⊢\left(A\in V\wedge B\in W\right)\to \left({2_{𝑜}}^{\left(B\times A\right)}\right)\approx \left({𝒫B}^A\right)$$
22		entr	$$⊢\left(𝒫\left(A\times B\right)\approx \left({2_{𝑜}}^{\left(B\times A\right)}\right)\wedge \left({2_{𝑜}}^{\left(B\times A\right)}\right)\approx \left({𝒫B}^A\right)\right)\to 𝒫\left(A\times B\right)\approx \left({𝒫B}^A\right)$$
23	9 21 22	syl2anc	$$⊢\left(A\in V\wedge B\in W\right)\to 𝒫\left(A\times B\right)\approx \left({𝒫B}^A\right)$$