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 = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 carw ⊢ Arrow
1 vc ⊢ 𝑐
2 ccat ⊢ Cat
3 choma ⊢ Homa
4 1 cv ⊢ 𝑐
5 4 3 cfv ⊢ ( Homa ‘ 𝑐 )
6 5 crn ⊢ ran ( Homa ‘ 𝑐 )
7 6 cuni ⊢ ∪ ran ( Homa ‘ 𝑐 )
8 1 2 7 cmpt ⊢ ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )
9 0 8 wceq ⊢ Arrow = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )