Metamath Proof Explorer

Theorem homahom2

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	homahom2	$⊢ Z (X H Y) F \to F \in (X J Y)$

Proof

Step	Hyp	Ref	Expression
1		homahom.h	$⊢ H = {Hom}_{a} (C)$
2		homahom.j	$⊢ J = Hom (C)$
3		df-br	$⊢ Z (X H Y) F \leftrightarrow ⟨Z, F⟩ \in (X H Y)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5	1	homarcl	$⊢ ⟨Z, F⟩ \in (X H Y) \to C \in Cat$
6	1 4	homarcl2	$⊢ ⟨Z, F⟩ \in (X H Y) \to (X \in {Base}_{C} \land Y \in {Base}_{C})$
7	6	simpld	$⊢ ⟨Z, F⟩ \in (X H Y) \to X \in {Base}_{C}$
8	6	simprd	$⊢ ⟨Z, F⟩ \in (X H Y) \to Y \in {Base}_{C}$
9	1 4 5 2 7 8	elhoma	$⊢ ⟨Z, F⟩ \in (X H Y) \to (Z (X H Y) F \leftrightarrow (Z = ⟨X, Y⟩ \land F \in (X J Y)))$
10	3 9	sylbi	$⊢ Z (X H Y) F \to (Z (X H Y) F \leftrightarrow (Z = ⟨X, Y⟩ \land F \in (X J Y)))$
11	10	ibi	$⊢ Z (X H Y) F \to (Z = ⟨X, Y⟩ \land F \in (X J Y))$
12	11	simprd	$⊢ Z (X H Y) F \to F \in (X J Y)$