Theorem elhomai2

Description: Produce an arrow from a morphism. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	homarcl.h	$$⊢H={Hom}_a\left(C\right)$$
	homafval.b	$$⊢B={\mathrm{Base}}_C$$
	homafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	homaval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
	homaval.x	$$⊢\phi \to X\in B$$
	homaval.y	$$⊢\phi \to Y\in B$$
	elhomai.f	$$⊢\phi \to F\in \left(XJY\right)$$
Assertion	elhomai2	$$⊢\phi \to ⟨X,Y,F⟩\in \left(XHY\right)$$

Proof

Step	Hyp	Ref	Expression
1		homarcl.h	$$⊢H={Hom}_a\left(C\right)$$
2		homafval.b	$$⊢B={\mathrm{Base}}_C$$
3		homafval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		homaval.j	$$⊢J=\mathrm{Hom}\left(C\right)$$
5		homaval.x	$$⊢\phi \to X\in B$$
6		homaval.y	$$⊢\phi \to Y\in B$$
7		elhomai.f	$$⊢\phi \to F\in \left(XJY\right)$$
8		df-ot	$$⊢⟨X,Y,F⟩=⟨⟨X,Y⟩,F⟩$$
9	1 2 3 4 5 6 7	elhomai	$$⊢\phi \to ⟨X,Y⟩\left(XHY\right)F$$
10		df-br	$$⊢⟨X,Y⟩\left(XHY\right)F\leftrightarrow ⟨⟨X,Y⟩,F⟩\in \left(XHY\right)$$
11	9 10	sylib	$$⊢\phi \to ⟨⟨X,Y⟩,F⟩\in \left(XHY\right)$$
12	8 11	eqeltrid	$$⊢\phi \to ⟨X,Y,F⟩\in \left(XHY\right)$$