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	|- A = ( Arrow ` C )
	arwhom.j	|- J = ( Hom ` C )
Assertion	arwhom	|- ( F e. A -> ( 2nd ` F ) e. ( ( domA ` F ) J ( codA ` F ) ) )

Proof

Step	Hyp	Ref	Expression
1		arwrcl.a	|- A = ( Arrow ` C )
2		arwhom.j	|- J = ( Hom ` C )
3		eqid	|- ( HomA ` C ) = ( HomA ` C )
4	1 3	arwhoma	|- ( F e. A -> F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) )
5	3 2	homahom	|- ( F e. ( ( domA ` F ) ( HomA ` C ) ( codA ` F ) ) -> ( 2nd ` F ) e. ( ( domA ` F ) J ( codA ` F ) ) )
6	4 5	syl	|- ( F e. A -> ( 2nd ` F ) e. ( ( domA ` F ) J ( codA ` F ) ) )