MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-func Structured version   Visualization version   GIF version

Definition df-func 17118
Description: Function returning all the functors from a category 𝑡 to a category 𝑢. Definition 3.17 of [Adamek] p. 29, and definition in [Lang] p. 62 ("covariant functor"). Intuitively a functor associates any morphism of 𝑡 to a morphism of 𝑢, any object of 𝑡 to an object of 𝑢, and respects the identity, the composition, the domain and the codomain. Here to capture the idea that a functor associates any object of 𝑡 to an object of 𝑢 we write it associates any identity of 𝑡 to an identity of 𝑢 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.)
Assertion
Ref Expression
df-func Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
Distinct variable group:   𝑓,𝑏,𝑔,𝑚,𝑛,𝑡,𝑢,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-func
StepHypRef Expression
1 cfunc 17114 . 2 class Func
2 vt . . 3 setvar 𝑡
3 vu . . 3 setvar 𝑢
4 ccat 16925 . . 3 class Cat
5 vb . . . . . . . 8 setvar 𝑏
65cv 1527 . . . . . . 7 class 𝑏
73cv 1527 . . . . . . . 8 class 𝑢
8 cbs 16473 . . . . . . . 8 class Base
97, 8cfv 6349 . . . . . . 7 class (Base‘𝑢)
10 vf . . . . . . . 8 setvar 𝑓
1110cv 1527 . . . . . . 7 class 𝑓
126, 9, 11wf 6345 . . . . . 6 wff 𝑓:𝑏⟶(Base‘𝑢)
13 vg . . . . . . . 8 setvar 𝑔
1413cv 1527 . . . . . . 7 class 𝑔
15 vz . . . . . . . 8 setvar 𝑧
166, 6cxp 5547 . . . . . . . 8 class (𝑏 × 𝑏)
1715cv 1527 . . . . . . . . . . . 12 class 𝑧
18 c1st 7678 . . . . . . . . . . . 12 class 1st
1917, 18cfv 6349 . . . . . . . . . . 11 class (1st𝑧)
2019, 11cfv 6349 . . . . . . . . . 10 class (𝑓‘(1st𝑧))
21 c2nd 7679 . . . . . . . . . . . 12 class 2nd
2217, 21cfv 6349 . . . . . . . . . . 11 class (2nd𝑧)
2322, 11cfv 6349 . . . . . . . . . 10 class (𝑓‘(2nd𝑧))
24 chom 16566 . . . . . . . . . . 11 class Hom
257, 24cfv 6349 . . . . . . . . . 10 class (Hom ‘𝑢)
2620, 23, 25co 7145 . . . . . . . . 9 class ((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧)))
272cv 1527 . . . . . . . . . . 11 class 𝑡
2827, 24cfv 6349 . . . . . . . . . 10 class (Hom ‘𝑡)
2917, 28cfv 6349 . . . . . . . . 9 class ((Hom ‘𝑡)‘𝑧)
30 cmap 8396 . . . . . . . . 9 class m
3126, 29, 30co 7145 . . . . . . . 8 class (((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
3215, 16, 31cixp 8450 . . . . . . 7 class X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
3314, 32wcel 2105 . . . . . 6 wff 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧))
34 vx . . . . . . . . . . . 12 setvar 𝑥
3534cv 1527 . . . . . . . . . . 11 class 𝑥
36 ccid 16926 . . . . . . . . . . . 12 class Id
3727, 36cfv 6349 . . . . . . . . . . 11 class (Id‘𝑡)
3835, 37cfv 6349 . . . . . . . . . 10 class ((Id‘𝑡)‘𝑥)
3935, 35, 14co 7145 . . . . . . . . . 10 class (𝑥𝑔𝑥)
4038, 39cfv 6349 . . . . . . . . 9 class ((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥))
4135, 11cfv 6349 . . . . . . . . . 10 class (𝑓𝑥)
427, 36cfv 6349 . . . . . . . . . 10 class (Id‘𝑢)
4341, 42cfv 6349 . . . . . . . . 9 class ((Id‘𝑢)‘(𝑓𝑥))
4440, 43wceq 1528 . . . . . . . 8 wff ((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥))
45 vn . . . . . . . . . . . . . . . 16 setvar 𝑛
4645cv 1527 . . . . . . . . . . . . . . 15 class 𝑛
47 vm . . . . . . . . . . . . . . . 16 setvar 𝑚
4847cv 1527 . . . . . . . . . . . . . . 15 class 𝑚
49 vy . . . . . . . . . . . . . . . . . 18 setvar 𝑦
5049cv 1527 . . . . . . . . . . . . . . . . 17 class 𝑦
5135, 50cop 4565 . . . . . . . . . . . . . . . 16 class 𝑥, 𝑦
52 cco 16567 . . . . . . . . . . . . . . . . 17 class comp
5327, 52cfv 6349 . . . . . . . . . . . . . . . 16 class (comp‘𝑡)
5451, 17, 53co 7145 . . . . . . . . . . . . . . 15 class (⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)
5546, 48, 54co 7145 . . . . . . . . . . . . . 14 class (𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)
5635, 17, 14co 7145 . . . . . . . . . . . . . 14 class (𝑥𝑔𝑧)
5755, 56cfv 6349 . . . . . . . . . . . . 13 class ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚))
5850, 17, 14co 7145 . . . . . . . . . . . . . . 15 class (𝑦𝑔𝑧)
5946, 58cfv 6349 . . . . . . . . . . . . . 14 class ((𝑦𝑔𝑧)‘𝑛)
6035, 50, 14co 7145 . . . . . . . . . . . . . . 15 class (𝑥𝑔𝑦)
6148, 60cfv 6349 . . . . . . . . . . . . . 14 class ((𝑥𝑔𝑦)‘𝑚)
6250, 11cfv 6349 . . . . . . . . . . . . . . . 16 class (𝑓𝑦)
6341, 62cop 4565 . . . . . . . . . . . . . . 15 class ⟨(𝑓𝑥), (𝑓𝑦)⟩
6417, 11cfv 6349 . . . . . . . . . . . . . . 15 class (𝑓𝑧)
657, 52cfv 6349 . . . . . . . . . . . . . . 15 class (comp‘𝑢)
6663, 64, 65co 7145 . . . . . . . . . . . . . 14 class (⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))
6759, 61, 66co 7145 . . . . . . . . . . . . 13 class (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
6857, 67wceq 1528 . . . . . . . . . . . 12 wff ((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
6950, 17, 28co 7145 . . . . . . . . . . . 12 class (𝑦(Hom ‘𝑡)𝑧)
7068, 45, 69wral 3138 . . . . . . . . . . 11 wff 𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
7135, 50, 28co 7145 . . . . . . . . . . 11 class (𝑥(Hom ‘𝑡)𝑦)
7270, 47, 71wral 3138 . . . . . . . . . 10 wff 𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
7372, 15, 6wral 3138 . . . . . . . . 9 wff 𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
7473, 49, 6wral 3138 . . . . . . . 8 wff 𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))
7544, 74wa 396 . . . . . . 7 wff (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
7675, 34, 6wral 3138 . . . . . 6 wff 𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚)))
7712, 33, 76w3a 1079 . . . . 5 wff (𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
7827, 8cfv 6349 . . . . 5 class (Base‘𝑡)
7977, 5, 78wsbc 3771 . . . 4 wff [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))
8079, 10, 13copab 5120 . . 3 class {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))}
812, 3, 4, 4, 80cmpo 7147 . 2 class (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
821, 81wceq 1528 1 wff Func = (𝑡 ∈ Cat, 𝑢 ∈ Cat ↦ {⟨𝑓, 𝑔⟩ ∣ [(Base‘𝑡) / 𝑏](𝑓:𝑏⟶(Base‘𝑢) ∧ 𝑔X𝑧 ∈ (𝑏 × 𝑏)(((𝑓‘(1st𝑧))(Hom ‘𝑢)(𝑓‘(2nd𝑧))) ↑m ((Hom ‘𝑡)‘𝑧)) ∧ ∀𝑥𝑏 (((𝑥𝑔𝑥)‘((Id‘𝑡)‘𝑥)) = ((Id‘𝑢)‘(𝑓𝑥)) ∧ ∀𝑦𝑏𝑧𝑏𝑚 ∈ (𝑥(Hom ‘𝑡)𝑦)∀𝑛 ∈ (𝑦(Hom ‘𝑡)𝑧)((𝑥𝑔𝑧)‘(𝑛(⟨𝑥, 𝑦⟩(comp‘𝑡)𝑧)𝑚)) = (((𝑦𝑔𝑧)‘𝑛)(⟨(𝑓𝑥), (𝑓𝑦)⟩(comp‘𝑢)(𝑓𝑧))((𝑥𝑔𝑦)‘𝑚))))})
Colors of variables: wff setvar class
This definition is referenced by:  relfunc  17122  funcrcl  17123  isfunc  17124
  Copyright terms: Public domain W3C validator