Theorem arwhom

Description: The second component of an arrow is the corresponding morphism (without the domain/codomain tag). (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
	arwhom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
Assertion	arwhom	⊢ ( 𝐹 ∈ 𝐴 → ( 2nd ‘ 𝐹 ) ∈ ( ( doma ‘ 𝐹 ) 𝐽 ( coda ‘ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	⊢ 𝐴 = ( Arrow ‘ 𝐶 )
2		arwhom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
3		eqid	⊢ ( Homa ‘ 𝐶 ) = ( Homa ‘ 𝐶 )
4	1 3	arwhoma	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ ( ( doma ‘ 𝐹 ) ( Homa ‘ 𝐶 ) ( coda ‘ 𝐹 ) ) )
5	3 2	homahom	⊢ ( 𝐹 ∈ ( ( doma ‘ 𝐹 ) ( Homa ‘ 𝐶 ) ( coda ‘ 𝐹 ) ) → ( 2nd ‘ 𝐹 ) ∈ ( ( doma ‘ 𝐹 ) 𝐽 ( coda ‘ 𝐹 ) ) )
6	4 5	syl	⊢ ( 𝐹 ∈ 𝐴 → ( 2nd ‘ 𝐹 ) ∈ ( ( doma ‘ 𝐹 ) 𝐽 ( coda ‘ 𝐹 ) ) )