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	⊢ ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cofc	⊢ ∘f/c 𝑅
2		vf	⊢ 𝑓
3		cvv	⊢ V
4		vc	⊢ 𝑐
5		vx	⊢ 𝑥
6	2	cv	⊢ 𝑓
7	6	cdm	⊢ dom 𝑓
8	5	cv	⊢ 𝑥
9	8 6	cfv	⊢ ( 𝑓 ‘ 𝑥 )
10	4	cv	⊢ 𝑐
11	9 10 0	co	⊢ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 )
12	5 7 11	cmpt	⊢ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) )
13	2 4 3 3 12	cmpo	⊢ ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )
14	1 13	wceq	⊢ ∘f/c 𝑅 = ( 𝑓 ∈ V , 𝑐 ∈ V ↦ ( 𝑥 ∈ dom 𝑓 ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 𝑐 ) ) )