homa1

Description: The first component of an arrow is the ordered pair of domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017)

		Ref	Expression
	Hypothesis	homahom.h	$⊢ H = {Hom}_{a} (C)$
	Assertion	homa1	$⊢ Z (X H Y) F \to Z = ⟨X, Y⟩$

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

Metamath Proof Explorer