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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1	0	cof	⊢ ∘f 𝑅
2		vf	⊢ 𝑓
3		cvv	⊢ V
4		vg	⊢ 𝑔
5		vx	⊢ 𝑥
6	2	cv	⊢ 𝑓
7	6	cdm	⊢ dom 𝑓
8	4	cv	⊢ 𝑔
9	8	cdm	⊢ dom 𝑔
10	7 9	cin	⊢ ( dom 𝑓 ∩ dom 𝑔 )
11	5	cv	⊢ 𝑥
12	11 6	cfv	⊢ ( 𝑓 ‘ 𝑥 )
13	11 8	cfv	⊢ ( 𝑔 ‘ 𝑥 )
14	12 13 0	co	⊢ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) )
15	5 10 14	cmpt	⊢ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) )
16	2 4 3 3 15	cmpo	⊢ ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )
17	1 16	wceq	⊢ ∘f 𝑅 = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ ( 𝑥 ∈ ( dom 𝑓 ∩ dom 𝑔 ) ↦ ( ( 𝑓 ‘ 𝑥 ) 𝑅 ( 𝑔 ‘ 𝑥 ) ) ) )