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 = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$

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 V$
4		vg	$setvar g$
5		vx	$setvar x$
6	2	cv	$setvar f$
7	6	cdm	$class dom f$
8	4	cv	$setvar g$
9	8	cdm	$class dom g$
10	7 9	cin	$class (dom f \cap dom g)$
11	5	cv	$setvar x$
12	11 6	cfv	$class f (x)$
13	11 8	cfv	$class g (x)$
14	12 13 0	co	$class (f (x) R g (x))$
15	5 10 14	cmpt	$class (x \in (dom f \cap dom g) ⟼ f (x) R g (x))$
16	2 4 3 3 15	cmpo	$class (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$
17	1 16	wceq	$wff \circ_{f} R = (f \in V, g \in V ⟼ (x \in (dom f \cap dom g) ⟼ f (x) R g (x)))$

Metamath Proof Explorer

Definition df-of

Detailed syntax breakdown