Metamath Proof Explorer

Theorem homahom

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	homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
		homahom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
	Assertion	homahom	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2^nd ‘ 𝐹 ) ∈ ( 𝑋 𝐽 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		homahom.h	⊢ 𝐻 = ( Hom_a ‘ 𝐶 )
2		homahom.j	⊢ 𝐽 = ( Hom ‘ 𝐶 )
3	1	homarel	⊢ Rel ( 𝑋 𝐻 𝑌 )
4		1st2ndbr	⊢ ( ( Rel ( 𝑋 𝐻 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
5	3 4	mpan	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) )
6	1 2	homahom2	⊢ ( ( 1^st ‘ 𝐹 ) ( 𝑋 𝐻 𝑌 ) ( 2^nd ‘ 𝐹 ) → ( 2^nd ‘ 𝐹 ) ∈ ( 𝑋 𝐽 𝑌 ) )
7	5 6	syl	⊢ ( 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) → ( 2^nd ‘ 𝐹 ) ∈ ( 𝑋 𝐽 𝑌 ) )