Theorem rfovfvfvd

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

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

Proof

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