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

Metamath Proof Explorer

Definition df-fuc

Description: Definition of the category of functors between two fixed categories, with the objects being functors and the morphisms being natural transformations. Definition 6.15 in Adamek p. 87. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion df-fuc FuncCat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfuc ⊢ FuncCat
1 vt ⊢ 𝑡
2 ccat ⊢ Cat
3 vu ⊢ 𝑢
4 cbs ⊢ Base
5 cnx ⊢ ndx
6 5 4 cfv ⊢ ( Base ‘ ndx )
7 1 cv ⊢ 𝑡
8 cfunc ⊢ Func
9 3 cv ⊢ 𝑢
10 7 9 8 co ⊢ ( 𝑡 Func 𝑢 )
11 6 10 cop ⊢ ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩
12 chom ⊢ Hom
13 5 12 cfv ⊢ ( Hom ‘ ndx )
14 cnat ⊢ Nat
15 7 9 14 co ⊢ ( 𝑡 Nat 𝑢 )
16 13 15 cop ⊢ ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩
17 cco ⊢ comp
18 5 17 cfv ⊢ ( comp ‘ ndx )
19 vv ⊢ 𝑣
20 10 10 cxp ⊢ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) )
21 vh ⊢ ℎ
22 c1st ⊢ 1st
23 19 cv ⊢ 𝑣
24 23 22 cfv ⊢ ( 1st ‘ 𝑣 )
25 vf ⊢ 𝑓
26 c2nd ⊢ 2nd
27 23 26 cfv ⊢ ( 2nd ‘ 𝑣 )
28 vg ⊢ 𝑔
29 vb ⊢ 𝑏
30 28 cv ⊢ 𝑔
31 21 cv ⊢ ℎ
32 30 31 15 co ⊢ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ )
33 va ⊢ 𝑎
34 25 cv ⊢ 𝑓
35 34 30 15 co ⊢ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 )
36 vx ⊢ 𝑥
37 7 4 cfv ⊢ ( Base ‘ 𝑡 )
38 29 cv ⊢ 𝑏
39 36 cv ⊢ 𝑥
40 39 38 cfv ⊢ ( 𝑏 ‘ 𝑥 )
41 34 22 cfv ⊢ ( 1st ‘ 𝑓 )
42 39 41 cfv ⊢ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 )
43 30 22 cfv ⊢ ( 1st ‘ 𝑔 )
44 39 43 cfv ⊢ ( ( 1st ‘ 𝑔 ) ‘ 𝑥 )
45 42 44 cop ⊢ ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩
46 9 17 cfv ⊢ ( comp ‘ 𝑢 )
47 31 22 cfv ⊢ ( 1st ‘ ℎ )
48 39 47 cfv ⊢ ( ( 1st ‘ ℎ ) ‘ 𝑥 )
49 45 48 46 co ⊢ ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) )
50 33 cv ⊢ 𝑎
51 39 50 cfv ⊢ ( 𝑎 ‘ 𝑥 )
52 40 51 49 co ⊢ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) )
53 36 37 52 cmpt ⊢ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) )
54 29 33 32 35 53 cmpo ⊢ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
55 28 27 54 csb ⊢ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
56 25 24 55 csb ⊢ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) )
57 19 21 20 10 56 cmpo ⊢ ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) )
58 18 57 cop ⊢ ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩
59 11 16 58 ctp ⊢ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ }
60 1 3 2 2 59 cmpo ⊢ ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )
61 0 60 wceq ⊢ FuncCat = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑡 Func 𝑢 ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑡 Nat 𝑢 ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑣 ∈ ( ( 𝑡 Func 𝑢 ) × ( 𝑡 Func 𝑢 ) ) , ℎ ∈ ( 𝑡 Func 𝑢 ) ↦ ⦋ ( 1st ‘ 𝑣 ) / 𝑓 ⦌ ⦋ ( 2nd ‘ 𝑣 ) / 𝑔 ⦌ ( 𝑏 ∈ ( 𝑔 ( 𝑡 Nat 𝑢 ) ℎ ) , 𝑎 ∈ ( 𝑓 ( 𝑡 Nat 𝑢 ) 𝑔 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑡 ) ↦ ( ( 𝑏 ‘ 𝑥 ) ( ⟨ ( ( 1st ‘ 𝑓 ) ‘ 𝑥 ) , ( ( 1st ‘ 𝑔 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝑢 ) ( ( 1st ‘ ℎ ) ‘ 𝑥 ) ) ( 𝑎 ‘ 𝑥 ) ) ) ) ) ⟩ } )