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	$⊢ H = {Hom}_{a} (C)$
		homahom.j	$⊢ J = Hom (C)$
	Assertion	homahom	$⊢ F \in (X H Y) \to 2^{nd} (F) \in (X J Y)$

Proof

Step	Hyp	Ref	Expression
1		homahom.h	$⊢ H = {Hom}_{a} (C)$
2		homahom.j	$⊢ J = Hom (C)$
3	1	homarel	$⊢ Rel (X H Y)$
4		1st2ndbr	$⊢ (Rel (X H Y) \land F \in (X H Y)) \to 1^{st} (F) (X H Y) 2^{nd} (F)$
5	3 4	mpan	$⊢ F \in (X H Y) \to 1^{st} (F) (X H Y) 2^{nd} (F)$
6	1 2	homahom2	$⊢ 1^{st} (F) (X H Y) 2^{nd} (F) \to 2^{nd} (F) \in (X J Y)$
7	5 6	syl	$⊢ F \in (X H Y) \to 2^{nd} (F) \in (X J Y)$