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

Metamath Proof Explorer

Theorem arwrcl

Description: The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Hypothesis	arwrcl.a	$⊢ A = Arrow (C)$
	Assertion	arwrcl	$⊢ F \in A \to C \in Cat$

Step	Hyp	Ref	Expression
1		arwrcl.a	$⊢ A = Arrow (C)$
2		df-arw	$⊢ Arrow = (c \in Cat ⟼ ⋃ ran {Hom}_{a} (c))$
3	2	dmmptss	$⊢ dom Arrow \subseteq Cat$
4		elfvdm	$⊢ F \in Arrow (C) \to C \in dom Arrow$
5	4 1	eleq2s	$⊢ F \in A \to C \in dom Arrow$
6	3 5	sselid	$⊢ F \in A \to C \in Cat$