Theorem rfovfvd

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

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

Proof

Step	Hyp	Ref	Expression
1		rfovd.rf	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑟 ∈ 𝒫 ( 𝑎 × 𝑏 ) ↦ ( 𝑥 ∈ 𝑎 ↦ { 𝑦 ∈ 𝑏 ∣ 𝑥 𝑟 𝑦 } ) ) )
2		rfovd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		rfovd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
4		rfovfvd.r	⊢ ( 𝜑 → 𝑅 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
5		rfovfvd.f	⊢ 𝐹 = ( 𝐴 𝑂 𝐵 )
6	1 2 3	rfovd	⊢ ( 𝜑 → ( 𝐴 𝑂 𝐵 ) = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
7	5 6	syl5eq	⊢ ( 𝜑 → 𝐹 = ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↦ ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) ) )
8		breq	⊢ ( 𝑟 = 𝑅 → ( 𝑥 𝑟 𝑦 ↔ 𝑥 𝑅 𝑦 ) )
9	8	rabbidv	⊢ ( 𝑟 = 𝑅 → { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } = { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑅 𝑦 } )
10	9	mpteq2dv	⊢ ( 𝑟 = 𝑅 → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑅 𝑦 } ) )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑟 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑅 𝑦 } ) )
12	2	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑅 𝑦 } ) ∈ V )
13	7 11 4 12	fvmptd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ { 𝑦 ∈ 𝐵 ∣ 𝑥 𝑅 𝑦 } ) )