Definition df-homa 17288

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 17286 and df-coda 17287. (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

Step	Hyp	Ref	Expression
1		choma 17285	. 2 class Homa
2		vc	. . 3 setvar 𝑐
3		ccat 16937	. . 3 class Cat
4		vx	. . . 4 setvar 𝑥
5	2	cv 1536	. . . . . 6 class 𝑐
6		cbs 16485	. . . . . 6 class Base
7	5, 6	cfv 6357	. . . . 5 class (Base‘𝑐)
8	7, 7	cxp 5555	. . . 4 class ((Base‘𝑐) × (Base‘𝑐))
9	4	cv 1536	. . . . . 6 class 𝑥
10	9	csn 4569	. . . . 5 class {𝑥}
11		chom 16578	. . . . . . 7 class Hom
12	5, 11	cfv 6357	. . . . . 6 class (Hom ‘𝑐)
13	9, 12	cfv 6357	. . . . 5 class ((Hom ‘𝑐)‘𝑥)
14	10, 13	cxp 5555	. . . 4 class ({𝑥} × ((Hom ‘𝑐)‘𝑥))
15	4, 8, 14	cmpt 5148	. . 3 class (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥)))
16	2, 3, 15	cmpt 5148	. 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))
17	1, 16	wceq 1537	1 wff Homa = (𝑐 ∈ Cat ↦ (𝑥 ∈ ((Base‘𝑐) × (Base‘𝑐)) ↦ ({𝑥} × ((Hom ‘𝑐)‘𝑥))))

This definition is referenced by:  homarcl  17290  homafval  17291  arwval  17305