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 ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
Assertion arwrcl ( 𝐹 ∈ 𝐴 → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 arwrcl.a ⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2 df-arw ⊢ Arrow = ( 𝑐 ∈ Cat ↦ ∪ ran ( Homa ‘ 𝑐 ) )
3 2 dmmptss ⊢ dom Arrow ⊆ Cat
4 elfvdm ⊢ ( 𝐹 ∈ ( Arrow ‘ 𝐶 ) → 𝐶 ∈ dom Arrow )
5 4 1 eleq2s ⊢ ( 𝐹 ∈ 𝐴 → 𝐶 ∈ dom Arrow )
6 3 5 sselid ⊢ ( 𝐹 ∈ 𝐴 → 𝐶 ∈ Cat )