Definition df-homa

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 and df-coda . (Contributed by FL, 6-May-2007) (Revised by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Assertion	df-homa	$$⊢{Hom}_a=\left(c\in \mathrm{Cat}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		choma	$$class{Hom}_a$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7	6 6	cxp	$$class\left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)$$
8	3	cv	$$setvarx$$
9	8	csn	$$class\left\{x\right\}$$
10		chom	$$class\mathrm{Hom}$$
11	5 10	cfv	$$class\mathrm{Hom}\left(c\right)$$
12	8 11	cfv	$$class\mathrm{Hom}\left(c\right)\left(x\right)$$
13	9 12	cxp	$$class\left(\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)$$
14	3 7 13	cmpt	$$class\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)$$
15	1 2 14	cmpt	$$class\left(c\in \mathrm{Cat}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)\right)$$
16	0 15	wceq	$$wff{Hom}_a=\left(c\in \mathrm{Cat}⟼\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_c\right)⟼\left\{x\right\}\times \mathrm{Hom}\left(c\right)\left(x\right)\right)\right)$$