Theorem subcss2

Description: The morphisms of a subcategory are a subset of the morphisms of the original. (Contributed by Mario Carneiro, 4-Jan-2017)

	Ref	Expression
Hypotheses	subcss1.1	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
	subcss1.2	$$⊢\phi \to JFn\left(S\times S\right)$$
	subcss2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
	subcss2.x	$$⊢\phi \to X\in S$$
	subcss2.y	$$⊢\phi \to Y\in S$$
Assertion	subcss2	$$⊢\phi \to XJY\subseteq XHY$$

Proof

Step	Hyp	Ref	Expression
1		subcss1.1	$$⊢\phi \to J\in \mathrm{Subcat}\left(C\right)$$
2		subcss1.2	$$⊢\phi \to JFn\left(S\times S\right)$$
3		subcss2.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
4		subcss2.x	$$⊢\phi \to X\in S$$
5		subcss2.y	$$⊢\phi \to Y\in S$$
6		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
7	1 6	subcssc	$$⊢\phi \to J{\subseteq }_{\mathrm{cat}}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
8	2 7 4 5	ssc2	$$⊢\phi \to XJY\subseteq X{\mathrm{Hom}}_{𝑓}\left(C\right)Y$$
9		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
10	1 2 9	subcss1	$$⊢\phi \to S\subseteq {\mathrm{Base}}_C$$
11	10 4	sseldd	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
12	10 5	sseldd	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
13	6 9 3 11 12	homfval	$$⊢\phi \to X{\mathrm{Hom}}_{𝑓}\left(C\right)Y=XHY$$
14	8 13	sseqtrd	$$⊢\phi \to XJY\subseteq XHY$$