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 ⁡ R = f g | ∀ x ∈ dom ⁡ f ∩ dom ⁡ g f ⁡ x R g ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 0 cofr class ∘ r ⁡ R
2 vf setvar f
3 vg setvar g
4 vx setvar x
5 2 cv setvar f
6 5 cdm class dom ⁡ f
7 3 cv setvar g
8 7 cdm class dom ⁡ g
9 6 8 cin class dom ⁡ f ∩ dom ⁡ g
10 4 cv setvar x
11 10 5 cfv class f ⁡ x
12 10 7 cfv class g ⁡ x
13 11 12 0 wbr wff f ⁡ x R g ⁡ x
14 13 4 9 wral wff ∀ x ∈ dom ⁡ f ∩ dom ⁡ g f ⁡ x R g ⁡ x
15 14 2 3 copab class f g | ∀ x ∈ dom ⁡ f ∩ dom ⁡ g f ⁡ x R g ⁡ x
16 1 15 wceq wff ∘ r ⁡ R = f g | ∀ x ∈ dom ⁡ f ∩ dom ⁡ g f ⁡ x R g ⁡ x