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

Definition df-hof 17098
 Description: Define the Hom functor, which is a bifunctor (a functor of two arguments), contravariant in the first argument and covariant in the second, from (oppCat‘𝐶) × 𝐶 to SetCat, whose object part is the hom-function Hom, and with morphism part given by pre- and post-composition. (Contributed by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-hof HomF = (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩)
Distinct variable group:   𝑏,𝑐,𝑓,𝑔,,𝑥,𝑦

Detailed syntax breakdown of Definition df-hof
StepHypRef Expression
1 chof 17096 . 2 class HomF
2 vc . . 3 setvar 𝑐
3 ccat 16532 . . 3 class Cat
42cv 1630 . . . . 5 class 𝑐
5 chomf 16534 . . . . 5 class Homf
64, 5cfv 6031 . . . 4 class (Homf𝑐)
7 vb . . . . 5 setvar 𝑏
8 cbs 16064 . . . . . 6 class Base
94, 8cfv 6031 . . . . 5 class (Base‘𝑐)
10 vx . . . . . 6 setvar 𝑥
11 vy . . . . . 6 setvar 𝑦
127cv 1630 . . . . . . 7 class 𝑏
1312, 12cxp 5247 . . . . . 6 class (𝑏 × 𝑏)
14 vf . . . . . . 7 setvar 𝑓
15 vg . . . . . . 7 setvar 𝑔
1611cv 1630 . . . . . . . . 9 class 𝑦
17 c1st 7313 . . . . . . . . 9 class 1st
1816, 17cfv 6031 . . . . . . . 8 class (1st𝑦)
1910cv 1630 . . . . . . . . 9 class 𝑥
2019, 17cfv 6031 . . . . . . . 8 class (1st𝑥)
21 chom 16160 . . . . . . . . 9 class Hom
224, 21cfv 6031 . . . . . . . 8 class (Hom ‘𝑐)
2318, 20, 22co 6793 . . . . . . 7 class ((1st𝑦)(Hom ‘𝑐)(1st𝑥))
24 c2nd 7314 . . . . . . . . 9 class 2nd
2519, 24cfv 6031 . . . . . . . 8 class (2nd𝑥)
2616, 24cfv 6031 . . . . . . . 8 class (2nd𝑦)
2725, 26, 22co 6793 . . . . . . 7 class ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦))
28 vh . . . . . . . 8 setvar
2919, 22cfv 6031 . . . . . . . 8 class ((Hom ‘𝑐)‘𝑥)
3015cv 1630 . . . . . . . . . 10 class 𝑔
3128cv 1630 . . . . . . . . . 10 class
32 cco 16161 . . . . . . . . . . . 12 class comp
334, 32cfv 6031 . . . . . . . . . . 11 class (comp‘𝑐)
3419, 26, 33co 6793 . . . . . . . . . 10 class (𝑥(comp‘𝑐)(2nd𝑦))
3530, 31, 34co 6793 . . . . . . . . 9 class (𝑔(𝑥(comp‘𝑐)(2nd𝑦)))
3614cv 1630 . . . . . . . . 9 class 𝑓
3718, 20cop 4322 . . . . . . . . . 10 class ⟨(1st𝑦), (1st𝑥)⟩
3837, 26, 33co 6793 . . . . . . . . 9 class (⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))
3935, 36, 38co 6793 . . . . . . . 8 class ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)
4028, 29, 39cmpt 4863 . . . . . . 7 class ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))
4114, 15, 23, 27, 40cmpt2 6795 . . . . . 6 class (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓)))
4210, 11, 13, 13, 41cmpt2 6795 . . . . 5 class (𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))
437, 9, 42csb 3682 . . . 4 class (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))
446, 43cop 4322 . . 3 class ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩
452, 3, 44cmpt 4863 . 2 class (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩)
461, 45wceq 1631 1 wff HomF = (𝑐 ∈ Cat ↦ ⟨(Homf𝑐), (Base‘𝑐) / 𝑏(𝑥 ∈ (𝑏 × 𝑏), 𝑦 ∈ (𝑏 × 𝑏) ↦ (𝑓 ∈ ((1st𝑦)(Hom ‘𝑐)(1st𝑥)), 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑐)(2nd𝑦)) ↦ ( ∈ ((Hom ‘𝑐)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝑐)(2nd𝑦)))(⟨(1st𝑦), (1st𝑥)⟩(comp‘𝑐)(2nd𝑦))𝑓))))⟩)
 Colors of variables: wff setvar class This definition is referenced by:  hofval  17100
 Copyright terms: Public domain W3C validator