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 ∈ Cat ⟼ ⋃ ran ⁡ Hom a ⁡ c

Detailed syntax breakdown

Step Hyp Ref Expression
0 carw class Arrow
1 vc setvar c
2 ccat class Cat
3 choma class Hom a
4 1 cv setvar c
5 4 3 cfv class Hom a ⁡ c
6 5 crn class ran ⁡ Hom a ⁡ c
7 6 cuni class ⋃ ran ⁡ Hom a ⁡ c
8 1 2 7 cmpt class c ∈ Cat ⟼ ⋃ ran ⁡ Hom a ⁡ c
9 0 8 wceq wff Arrow = c ∈ Cat ⟼ ⋃ ran ⁡ Hom a ⁡ c