This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑔 ) ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) }