Definition df-ofc 32064

Description: Define the function/constant operation map. The definition is designed so that if 𝑅 is a binary operation, then ∘_f/c 𝑅 is the analogous operation on functions and constants. (Contributed by Thierry Arnoux, 21-Jan-2017.)

Assertion

Ref	Expression
df-ofc	⊢ ∘f/c 𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)))

Distinct variable group:   𝑓,𝑐,𝑥,𝑅

Detailed syntax breakdown of Definition df-ofc

Step	Hyp	Ref	Expression
1		cR	. . 3 class 𝑅
2	1	cofc 32063	. 2 class ∘f/c 𝑅
3		vf	. . 3 setvar 𝑓
4		vc	. . 3 setvar 𝑐
5		cvv 3432	. . 3 class V
6		vx	. . . 4 setvar 𝑥
7	3	cv 1538	. . . . 5 class 𝑓
8	7	cdm 5589	. . . 4 class dom 𝑓
9	6	cv 1538	. . . . . 6 class 𝑥
10	9, 7	cfv 6433	. . . . 5 class (𝑓‘𝑥)
11	4	cv 1538	. . . . 5 class 𝑐
12	10, 11, 1	co 7275	. . . 4 class ((𝑓‘𝑥)𝑅𝑐)
13	6, 8, 12	cmpt 5157	. . 3 class (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐))
14	3, 4, 5, 5, 13	cmpo 7277	. 2 class (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)))
15	2, 14	wceq 1539	1 wff ∘f/c 𝑅 = (𝑓 ∈ V, 𝑐 ∈ V ↦ (𝑥 ∈ dom 𝑓 ↦ ((𝑓‘𝑥)𝑅𝑐)))

This definition is referenced by:  ofceq  32065  ofcfval  32066  ofcfval3  32070