Definition df-ofc

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

	Ref	Expression
Assertion	df-ofc	|- oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	|- R
1	0	cofc	|- oFC R
2		vf	|- f
3		cvv	|- _V
4		vc	|- c
5		vx	|- x
6	2	cv	|- f
7	6	cdm	|- dom f
8	5	cv	|- x
9	8 6	cfv	|- ( f ` x )
10	4	cv	|- c
11	9 10 0	co	|- ( ( f ` x ) R c )
12	5 7 11	cmpt	|- ( x e. dom f |-> ( ( f ` x ) R c ) )
13	2 4 3 3 12	cmpo	|- ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )
14	1 13	wceq	|- oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )