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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 𝒫 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		xpcomeng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) )
2		pwen	⊢ ( ( 𝐴 × 𝐵 ) ≈ ( 𝐵 × 𝐴 ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ 𝒫 ( 𝐵 × 𝐴 ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ 𝒫 ( 𝐵 × 𝐴 ) )
4		xpexg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 × 𝐴 ) ∈ V )
5	4	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × 𝐴 ) ∈ V )
6		pw2eng	⊢ ( ( 𝐵 × 𝐴 ) ∈ V → 𝒫 ( 𝐵 × 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
7	5 6	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐵 × 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
8		entr	⊢ ( ( 𝒫 ( 𝐴 × 𝐵 ) ≈ 𝒫 ( 𝐵 × 𝐴 ) ∧ 𝒫 ( 𝐵 × 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
9	3 7 8	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
10		pw2eng	⊢ ( 𝐵 ∈ 𝑊 → 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) )
11		enrefg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 )
12		mapen	⊢ ( ( 𝒫 𝐵 ≈ ( 2o ↑m 𝐵 ) ∧ 𝐴 ≈ 𝐴 ) → ( 𝒫 𝐵 ↑m 𝐴 ) ≈ ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) )
13	10 11 12	syl2anr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐵 ↑m 𝐴 ) ≈ ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) )
14		2on	⊢ 2o ∈ On
15		simpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
16		simpl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 )
17		mapxpen	⊢ ( ( 2o ∈ On ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
18	14 15 16 17	mp3an2i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
19		entr	⊢ ( ( ( 𝒫 𝐵 ↑m 𝐴 ) ≈ ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) ∧ ( ( 2o ↑m 𝐵 ) ↑m 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) ) → ( 𝒫 𝐵 ↑m 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
20	13 18 19	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐵 ↑m 𝐴 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) )
21	20	ensymd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 2o ↑m ( 𝐵 × 𝐴 ) ) ≈ ( 𝒫 𝐵 ↑m 𝐴 ) )
22		entr	⊢ ( ( 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 2o ↑m ( 𝐵 × 𝐴 ) ) ∧ ( 2o ↑m ( 𝐵 × 𝐴 ) ) ≈ ( 𝒫 𝐵 ↑m 𝐴 ) ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 𝒫 𝐵 ↑m 𝐴 ) )
23	9 21 22	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ≈ ( 𝒫 𝐵 ↑m 𝐴 ) )