This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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