# Metamath Proof Explorer

## Definition df-of

Description: Define the function operation map. The definition is designed so that if R is a binary operation, then oF R is the analogous operation on functions which corresponds to applying R pointwise to the values of the functions. (Contributed by Mario Carneiro, 20-Jul-2014)

Ref Expression
Assertion df-of ${⊢}{\circ }_{f}{R}=\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ${class}{R}$
1 0 cof ${class}{\circ }_{f}{R}$
2 vf ${setvar}{f}$
3 cvv ${class}\mathrm{V}$
4 vg ${setvar}{g}$
5 vx ${setvar}{x}$
6 2 cv ${setvar}{f}$
7 6 cdm ${class}\mathrm{dom}{f}$
8 4 cv ${setvar}{g}$
9 8 cdm ${class}\mathrm{dom}{g}$
10 7 9 cin ${class}\left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)$
11 5 cv ${setvar}{x}$
12 11 6 cfv ${class}{f}\left({x}\right)$
13 11 8 cfv ${class}{g}\left({x}\right)$
14 12 13 0 co ${class}\left({f}\left({x}\right){R}{g}\left({x}\right)\right)$
15 5 10 14 cmpt ${class}\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)$
16 2 4 3 3 15 cmpo ${class}\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$
17 1 16 wceq ${wff}{\circ }_{f}{R}=\left({f}\in \mathrm{V},{g}\in \mathrm{V}⟼\left({x}\in \left(\mathrm{dom}{f}\cap \mathrm{dom}{g}\right)⟼{f}\left({x}\right){R}{g}\left({x}\right)\right)\right)$