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 = t ∈ Cat , u ∈ Cat ⟼ Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfuc class FuncCat
1 vt setvar t
2 ccat class Cat
3 vu setvar u
4 cbs class Base
5 cnx class ndx
6 5 4 cfv class Base ndx
7 1 cv setvar t
8 cfunc class Func
9 3 cv setvar u
10 7 9 8 co class t Func u
11 6 10 cop class Base ndx t Func u
12 chom class Hom
13 5 12 cfv class Hom ⁡ ndx
14 cnat class Nat
15 7 9 14 co class t Nat u
16 13 15 cop class Hom ⁡ ndx t Nat u
17 cco class comp
18 5 17 cfv class comp ⁡ ndx
19 vv setvar v
20 10 10 cxp class t Func u × t Func u
21 vh setvar h
22 c1st class 1 st
23 19 cv setvar v
24 23 22 cfv class 1 st ⁡ v
25 vf setvar f
26 c2nd class 2 nd
27 23 26 cfv class 2 nd ⁡ v
28 vg setvar g
29 vb setvar b
30 28 cv setvar g
31 21 cv setvar h
32 30 31 15 co class g t Nat u h
33 va setvar a
34 25 cv setvar f
35 34 30 15 co class f t Nat u g
36 vx setvar x
37 7 4 cfv class Base t
38 29 cv setvar b
39 36 cv setvar x
40 39 38 cfv class b ⁡ x
41 34 22 cfv class 1 st ⁡ f
42 39 41 cfv class 1 st ⁡ f ⁡ x
43 30 22 cfv class 1 st ⁡ g
44 39 43 cfv class 1 st ⁡ g ⁡ x
45 42 44 cop class 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x
46 9 17 cfv class comp ⁡ u
47 31 22 cfv class 1 st ⁡ h
48 39 47 cfv class 1 st ⁡ h ⁡ x
49 45 48 46 co class 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x
50 33 cv setvar a
51 39 50 cfv class a ⁡ x
52 40 51 49 co class b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
53 36 37 52 cmpt class x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
54 29 33 32 35 53 cmpo class b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
55 28 27 54 csb class ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
56 25 24 55 csb class ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
57 19 21 20 10 56 cmpo class v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
58 18 57 cop class comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
59 11 16 58 ctp class Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
60 1 3 2 2 59 cmpo class t ∈ Cat , u ∈ Cat ⟼ Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x
61 0 60 wceq wff FuncCat = t ∈ Cat , u ∈ Cat ⟼ Base ndx t Func u Hom ⁡ ndx t Nat u comp ⁡ ndx v ∈ t Func u × t Func u , h ∈ t Func u ⟼ ⦋ 1 st ⁡ v / f⦌ ⦋ 2 nd ⁡ v / g⦌ b ∈ g t Nat u h , a ∈ f t Nat u g ⟼ x ∈ Base t ⟼ b ⁡ x 1 st ⁡ f ⁡ x 1 st ⁡ g ⁡ x comp ⁡ u 1 st ⁡ h ⁡ x a ⁡ x