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	\|- HomA = ( c e. Cat \|-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) \|-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		choma	\|- HomA
1		vc	\|- c
2		ccat	\|- Cat
3		vx	\|- x
4		cbs	\|- Base
5	1	cv	\|- c
6	5 4	cfv	\|- ( Base ` c )
7	6 6	cxp	\|- ( ( Base ` c ) X. ( Base ` c ) )
8	3	cv	\|- x
9	8	csn	\|- { x }
10		chom	\|- Hom
11	5 10	cfv	\|- ( Hom ` c )
12	8 11	cfv	\|- ( ( Hom ` c ) ` x )
13	9 12	cxp	\|- ( { x } X. ( ( Hom ` c ) ` x ) )
14	3 7 13	cmpt	\|- ( x e. ( ( Base ` c ) X. ( Base ` c ) ) \|-> ( { x } X. ( ( Hom ` c ) ` x ) ) )
15	1 2 14	cmpt	\|- ( c e. Cat \|-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) \|-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )
16	0 15	wceq	\|- HomA = ( c e. Cat \|-> ( x e. ( ( Base ` c ) X. ( Base ` c ) ) \|-> ( { x } X. ( ( Hom ` c ) ` x ) ) ) )

Metamath Proof Explorer

Definition df-homa

Detailed syntax breakdown