Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-homa | Structured version Visualization version GIF version |
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 17727 and df-coda 17728. (Contributed by FL, 6-May-2007.) (Revised by Mario Carneiro, 11-Jan-2017.) |
Ref | Expression |
---|---|
df-homa | ⊢ Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | choma 17726 | . 2 class Homa | |
2 | vc | . . 3 setvar 𝑐 | |
3 | ccat 17361 | . . 3 class Cat | |
4 | vx | . . . 4 setvar 𝑥 | |
5 | 2 | cv 1538 | . . . . . 6 class 𝑐 |
6 | cbs 16900 | . . . . . 6 class Base | |
7 | 5, 6 | cfv 6427 | . . . . 5 class (Base‘𝑐) |
8 | 7, 7 | cxp 5583 | . . . 4 class ((Base‘𝑐) × (Base‘𝑐)) |
9 | 4 | cv 1538 | . . . . . 6 class 𝑥 |
10 | 9 | csn 4562 | . . . . 5 class {𝑥} |
11 | chom 16961 | . . . . . . 7 class Hom | |
12 | 5, 11 | cfv 6427 | . . . . . 6 class (Hom ‘𝑐) |
13 | 9, 12 | cfv 6427 | . . . . 5 class ((Hom ‘𝑐)‘𝑥) |
14 | 10, 13 | cxp 5583 | . . . 4 class ({𝑥} × ((Hom ‘𝑐)‘𝑥)) |
15 | 4, 8, 14 | cmpt 5157 | . . 3 class (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))) |
16 | 2, 3, 15 | cmpt 5157 | . 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) |
17 | 1, 16 | wceq 1539 | 1 wff Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))) |
Colors of variables: wff setvar class |
This definition is referenced by: homarcl 17731 homafval 17732 arwval 17746 |
Copyright terms: Public domain | W3C validator |