Metamath Proof Explorer


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 ‘ 𝑐 ) 𝑦 ) 𝑓 ) ) ) )