Theorem hof1

Description: The object part of the Hom functor maps X , Y to the set of morphisms from X to Y . (Contributed by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	hofval.m	$$⊢M={Hom}_F\left(C\right)$$
	hofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	hof1.b	$$⊢B={\mathrm{Base}}_C$$
	hof1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	hof1.x	$$⊢\phi \to X\in B$$
	hof1.y	$$⊢\phi \to Y\in B$$
Assertion	hof1	$$⊢\phi \to X{1}^{st}\left(M\right)Y=XHY$$

Proof

Step	Hyp	Ref	Expression
1		hofval.m	$$⊢M={Hom}_F\left(C\right)$$
2		hofval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		hof1.b	$$⊢B={\mathrm{Base}}_C$$
4		hof1.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
5		hof1.x	$$⊢\phi \to X\in B$$
6		hof1.y	$$⊢\phi \to Y\in B$$
7	1 2	hof1fval	$$⊢\phi \to 1^{st}\left(M\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
8	7	oveqd	$$⊢\phi \to X{1}^{st}\left(M\right)Y=X{\mathrm{Hom}}_{𝑓}\left(C\right)Y$$
9		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
10	9 3 4 5 6	homfval	$$⊢\phi \to X{\mathrm{Hom}}_{𝑓}\left(C\right)Y=XHY$$
11	8 10	eqtrd	$$⊢\phi \to X{1}^{st}\left(M\right)Y=XHY$$