Theorem elhomai

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	elhomai	$$⊢\phi \to ⟨X,Y⟩\left(XHY\right)F$$

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		eqidd	$$⊢\phi \to ⟨X,Y⟩=⟨X,Y⟩$$
9	1 2 3 4 5 6	elhoma	$$⊢\phi \to \left(⟨X,Y⟩\left(XHY\right)F\leftrightarrow \left(⟨X,Y⟩=⟨X,Y⟩\wedge F\in \left(XJY\right)\right)\right)$$
10	8 7 9	mpbir2and	$$⊢\phi \to ⟨X,Y⟩\left(XHY\right)F$$