Definition df-ofr

Description: Define the function relation map. The definition is designed so that if R is a binary relation, then oR R is the analogous relation on functions which is true when each element of the left function relates to the corresponding element of the right function. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	df-ofr	⊢ ∘r 𝑅 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cofr	⊢ ∘r 𝑅
2		vf	⊢ 𝑓
3		vg	⊢ 𝑔
4		vx	⊢ 𝑥
5	2	cv	⊢ 𝑓
6	5	cdm	⊢ dom 𝑓
7	3	cv	⊢ 𝑔
8	7	cdm	⊢ dom 𝑔
9	6 8	cin	⊢ ( dom 𝑓 ∩ dom 𝑔 )
10	4	cv	⊢ 𝑥
11	10 5	cfv	⊢ ( 𝑓 ‘ 𝑥 )
12	10 7	cfv	⊢ ( 𝑔 ‘ 𝑥 )
13	11 12 0	wbr	⊢ ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 )
14	13 4 9	wral	⊢ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 )
15	14 2 3	copab	⊢ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) }
16	1 15	wceq	⊢ ∘r 𝑅 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ∀ 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) }