Metamath Proof Explorer

Definition df-func

Description: Function returning all the functors from a category t to a category u . Definition 3.17 of Adamek p. 29, and definition in Lang p. 62 ("covariant functor"). Intuitively a functor associates any morphism of t to a morphism of u , any object of t to an object of u , and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of t to an object of u we write it associates any identity of t to an identity of u which simplifies the definition. According to remark 3.19 in Adamek p. 30, "a functor F : A -> B is technically a family of functions; one from Ob(A) to Ob(B) [here: f, called "the object part" in the following], and for each pair (A,A') of A-objects, one from hom(A,A') to hom(FA, FA') [here: g, called "the morphism part" in the following]". (Contributed by FL, 10-Feb-2008) (Revised by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion df-func ⊢ Func = t ∈ Cat , u ∈ Cat ⟼ f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfunc class Func
1 vt setvar t
2 ccat class Cat
3 vu setvar u
4 vf setvar f
5 vg setvar g
6 cbs class Base
7 1 cv setvar t
8 7 6 cfv class Base t
9 vb setvar b
10 4 cv setvar f
11 9 cv setvar b
12 3 cv setvar u
13 12 6 cfv class Base u
14 11 13 10 wf wff f : b ⟶ Base u
15 5 cv setvar g
16 vz setvar z
17 11 11 cxp class b × b
18 c1st class 1 st
19 16 cv setvar z
20 19 18 cfv class 1 st ⁡ z
21 20 10 cfv class f ⁡ 1 st ⁡ z
22 chom class Hom
23 12 22 cfv class Hom ⁡ u
24 c2nd class 2 nd
25 19 24 cfv class 2 nd ⁡ z
26 25 10 cfv class f ⁡ 2 nd ⁡ z
27 21 26 23 co class f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z
28 cmap class ↑ 𝑚
29 7 22 cfv class Hom ⁡ t
30 19 29 cfv class Hom ⁡ t ⁡ z
31 27 30 28 co class f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z
32 16 17 31 cixp class ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z
33 15 32 wcel wff g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z
34 vx setvar x
35 34 cv setvar x
36 35 35 15 co class x g x
37 ccid class Id
38 7 37 cfv class Id ⁡ t
39 35 38 cfv class Id ⁡ t ⁡ x
40 39 36 cfv class x g x ⁡ Id ⁡ t ⁡ x
41 12 37 cfv class Id ⁡ u
42 35 10 cfv class f ⁡ x
43 42 41 cfv class Id ⁡ u ⁡ f ⁡ x
44 40 43 wceq wff x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x
45 vy setvar y
46 vm setvar m
47 45 cv setvar y
48 35 47 29 co class x Hom ⁡ t y
49 vn setvar n
50 47 19 29 co class y Hom ⁡ t z
51 35 19 15 co class x g z
52 49 cv setvar n
53 35 47 cop class x y
54 cco class comp
55 7 54 cfv class comp ⁡ t
56 53 19 55 co class x y comp ⁡ t z
57 46 cv setvar m
58 52 57 56 co class n x y comp ⁡ t z m
59 58 51 cfv class x g z ⁡ n x y comp ⁡ t z m
60 47 19 15 co class y g z
61 52 60 cfv class y g z ⁡ n
62 47 10 cfv class f ⁡ y
63 42 62 cop class f ⁡ x f ⁡ y
64 12 54 cfv class comp ⁡ u
65 19 10 cfv class f ⁡ z
66 63 65 64 co class f ⁡ x f ⁡ y comp ⁡ u f ⁡ z
67 35 47 15 co class x g y
68 57 67 cfv class x g y ⁡ m
69 61 68 66 co class y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
70 59 69 wceq wff x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
71 70 49 50 wral wff ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
72 71 46 48 wral wff ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
73 72 16 11 wral wff ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
74 73 45 11 wral wff ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
75 44 74 wa wff x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
76 75 34 11 wral wff ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
77 14 33 76 w3a wff f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
78 77 9 8 wsbc wff [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
79 78 4 5 copab class f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
80 1 3 2 2 79 cmpo class t ∈ Cat , u ∈ Cat ⟼ f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
81 0 80 wceq wff Func = t ∈ Cat , u ∈ Cat ⟼ f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m