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

Definition df-hof 18144
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 18142 . 2 class HomF
2 vc . . 3 setvar 𝑐
3 ccat 17549 . . 3 class Cat
42cv 1541 . . . . 5 class 𝑐
5 chomf 17551 . . . . 5 class Homf
64, 5cfv 6497 . . . 4 class (Homf β€˜π‘)
7 vb . . . . 5 setvar 𝑏
8 cbs 17088 . . . . . 6 class Base
94, 8cfv 6497 . . . . 5 class (Baseβ€˜π‘)
10 vx . . . . . 6 setvar π‘₯
11 vy . . . . . 6 setvar 𝑦
127cv 1541 . . . . . . 7 class 𝑏
1312, 12cxp 5632 . . . . . 6 class (𝑏 Γ— 𝑏)
14 vf . . . . . . 7 setvar 𝑓
15 vg . . . . . . 7 setvar 𝑔
1611cv 1541 . . . . . . . . 9 class 𝑦
17 c1st 7920 . . . . . . . . 9 class 1st
1816, 17cfv 6497 . . . . . . . 8 class (1st β€˜π‘¦)
1910cv 1541 . . . . . . . . 9 class π‘₯
2019, 17cfv 6497 . . . . . . . 8 class (1st β€˜π‘₯)
21 chom 17149 . . . . . . . . 9 class Hom
224, 21cfv 6497 . . . . . . . 8 class (Hom β€˜π‘)
2318, 20, 22co 7358 . . . . . . 7 class ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯))
24 c2nd 7921 . . . . . . . . 9 class 2nd
2519, 24cfv 6497 . . . . . . . 8 class (2nd β€˜π‘₯)
2616, 24cfv 6497 . . . . . . . 8 class (2nd β€˜π‘¦)
2725, 26, 22co 7358 . . . . . . 7 class ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦))
28 vh . . . . . . . 8 setvar β„Ž
2919, 22cfv 6497 . . . . . . . 8 class ((Hom β€˜π‘)β€˜π‘₯)
3015cv 1541 . . . . . . . . . 10 class 𝑔
3128cv 1541 . . . . . . . . . 10 class β„Ž
32 cco 17150 . . . . . . . . . . . 12 class comp
334, 32cfv 6497 . . . . . . . . . . 11 class (compβ€˜π‘)
3419, 26, 33co 7358 . . . . . . . . . 10 class (π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))
3530, 31, 34co 7358 . . . . . . . . 9 class (𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)
3614cv 1541 . . . . . . . . 9 class 𝑓
3718, 20cop 4593 . . . . . . . . . 10 class ⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩
3837, 26, 33co 7358 . . . . . . . . 9 class (⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))
3935, 36, 38co 7358 . . . . . . . 8 class ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓)
4028, 29, 39cmpt 5189 . . . . . . 7 class (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))
4114, 15, 23, 27, 40cmpo 7360 . . . . . 6 class (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓)))
4210, 11, 13, 13, 41cmpo 7360 . . . . 5 class (π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ (𝑏 Γ— 𝑏) ↦ (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))))
437, 9, 42csb 3856 . . . 4 class ⦋(Baseβ€˜π‘) / π‘β¦Œ(π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ (𝑏 Γ— 𝑏) ↦ (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))))
446, 43cop 4593 . . 3 class ⟨(Homf β€˜π‘), ⦋(Baseβ€˜π‘) / π‘β¦Œ(π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ (𝑏 Γ— 𝑏) ↦ (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))))⟩
452, 3, 44cmpt 5189 . 2 class (𝑐 ∈ Cat ↦ ⟨(Homf β€˜π‘), ⦋(Baseβ€˜π‘) / π‘β¦Œ(π‘₯ ∈ (𝑏 Γ— 𝑏), 𝑦 ∈ (𝑏 Γ— 𝑏) ↦ (𝑓 ∈ ((1st β€˜π‘¦)(Hom β€˜π‘)(1st β€˜π‘₯)), 𝑔 ∈ ((2nd β€˜π‘₯)(Hom β€˜π‘)(2nd β€˜π‘¦)) ↦ (β„Ž ∈ ((Hom β€˜π‘)β€˜π‘₯) ↦ ((𝑔(π‘₯(compβ€˜π‘)(2nd β€˜π‘¦))β„Ž)(⟨(1st β€˜π‘¦), (1st β€˜π‘₯)⟩(compβ€˜π‘)(2nd β€˜π‘¦))𝑓))))⟩)
461, 45wceq 1542 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  18146
  Copyright terms: Public domain W3C validator