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

Definition df-homa 16723
Description: Definition of the hom-set extractor for arrows, which tags the morphisms of the underlying hom-set with domain and codomain, which can then be extracted using df-doma 16721 and df-coda 16722. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.)
Assertion
Ref Expression
df-homa Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-homa
StepHypRef Expression
1 choma 16720 . 2 class Homa
2 vc . . 3 setvar 𝑐
3 ccat 16372 . . 3 class Cat
4 vx . . . 4 setvar 𝑥
52cv 1522 . . . . . 6 class 𝑐
6 cbs 15904 . . . . . 6 class Base
75, 6cfv 5926 . . . . 5 class (Base‘𝑐)
87, 7cxp 5141 . . . 4 class ((Base‘𝑐) × (Base‘𝑐))
94cv 1522 . . . . . 6 class 𝑥
109csn 4210 . . . . 5 class {𝑥}
11 chom 15999 . . . . . . 7 class Hom
125, 11cfv 5926 . . . . . 6 class (Hom ‘𝑐)
139, 12cfv 5926 . . . . 5 class ((Hom ‘𝑐)‘𝑥)
1410, 13cxp 5141 . . . 4 class ({𝑥} × ((Hom ‘𝑐)‘𝑥))
154, 8, 14cmpt 4762 . . 3 class (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))
162, 3, 15cmpt 4762 . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
171, 16wceq 1523 1 wff Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
Colors of variables: wff setvar class
This definition is referenced by:  homarcl  16725  homafval  16726  arwval  16740
  Copyright terms: Public domain W3C validator