Definition df-comf

Description: Define the functionalized composition operator, which is exactly like comp but is guaranteed to be a function of the proper type. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Assertion	df-comf	⊢ compf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccomf	⊢ compf
1		vc	⊢ 𝑐
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7	6 6	cxp	⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) )
8		vy	⊢ 𝑦
9		vg	⊢ 𝑔
10		c2nd	⊢ 2nd
11	3	cv	⊢ 𝑥
12	11 10	cfv	⊢ ( 2nd ‘ 𝑥 )
13		chom	⊢ Hom
14	5 13	cfv	⊢ ( Hom ‘ 𝑐 )
15	8	cv	⊢ 𝑦
16	12 15 14	co	⊢ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 )
17		vf	⊢ 𝑓
18	11 14	cfv	⊢ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 )
19	9	cv	⊢ 𝑔
20		cco	⊢ comp
21	5 20	cfv	⊢ ( comp ‘ 𝑐 )
22	11 15 21	co	⊢ ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 )
23	17	cv	⊢ 𝑓
24	19 23 22	co	⊢ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 )
25	9 17 16 18 24	cmpo	⊢ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) )
26	3 8 7 6 25	cmpo	⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) )
27	1 2 26	cmpt	⊢ ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) )
28	0 27	wceq	⊢ compf = ( 𝑐 ∈ V ↦ ( 𝑥 ∈ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑐 ) ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ ( 𝑔 ∈ ( ( 2nd ‘ 𝑥 ) ( Hom ‘ 𝑐 ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ 𝑐 ) ‘ 𝑥 ) ↦ ( 𝑔 ( 𝑥 ( comp ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) )