Theorem rfovd

Description: Value of the operator, ( A O B ) , which maps between relations and functions for relations between base sets, A and B . (Contributed by RP, 25-Apr-2021)

	Ref	Expression
Hypotheses	rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
	rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	rfovd	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
2		rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4	1	a1i	⊢ ( 𝜑 → 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) ) )
5		xpeq12	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 × 𝑏 ) = ( 𝐴 × 𝐵 ) )
6	5	pweqd	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝒫 ( 𝑎 × 𝑏 ) = 𝒫 ( 𝐴 × 𝐵 ) )
7		simpl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝐴 )
8		rabeq	⊢ ( 𝑏 = 𝐵 → { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
9	8	adantl	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } )
10	7 9	mpteq12dv	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) )
11	6 10	mpteq12dv	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
13	2	elexd	⊢ ( 𝜑 → 𝐴 ∈ V )
14	3	elexd	⊢ ( 𝜑 → 𝐵 ∈ V )
15	2 3	xpexd	⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
16		pwexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
17		mptexg	⊢ ( 𝒫 ( 𝐴 × 𝐵 ) ∈ V → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∈ V )
18	15 16 17	3syl	⊢ ( 𝜑 → ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) ∈ V )
19	4 12 13 14 18	ovmpod	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )