This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-arw

Description: Definition of the set of arrows of a category. We will use the term "arrow" to denote a morphism tagged with its domain and codomain, as opposed to Hom , which allows hom-sets for distinct objects to overlap. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Assertion	df-arw	\|- Arrow = ( c e. Cat \|-> U. ran ( HomA ` c ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carw	\|- Arrow
1		vc	\|- c
2		ccat	\|- Cat
3		choma	\|- HomA
4	1	cv	\|- c
5	4 3	cfv	\|- ( HomA ` c )
6	5	crn	\|- ran ( HomA ` c )
7	6	cuni	\|- U. ran ( HomA ` c )
8	1 2 7	cmpt	\|- ( c e. Cat \|-> U. ran ( HomA ` c ) )
9	0 8	wceq	\|- Arrow = ( c e. Cat \|-> U. ran ( HomA ` c ) )