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	|- ( ph -> J e. ( Subcat ` C ) )
	subcss1.2	|- ( ph -> J Fn ( S X. S ) )
	subcss2.h	|- H = ( Hom ` C )
	subcss2.x	|- ( ph -> X e. S )
	subcss2.y	|- ( ph -> Y e. S )
Assertion	subcss2	|- ( ph -> ( X J Y ) C_ ( X H Y ) )

Proof

Step	Hyp	Ref	Expression
1		subcss1.1	|- ( ph -> J e. ( Subcat ` C ) )
2		subcss1.2	|- ( ph -> J Fn ( S X. S ) )
3		subcss2.h	|- H = ( Hom ` C )
4		subcss2.x	|- ( ph -> X e. S )
5		subcss2.y	|- ( ph -> Y e. S )
6		eqid	|- ( Homf ` C ) = ( Homf ` C )
7	1 6	subcssc	|- ( ph -> J C_cat ( Homf ` C ) )
8	2 7 4 5	ssc2	|- ( ph -> ( X J Y ) C_ ( X ( Homf ` C ) Y ) )
9		eqid	|- ( Base ` C ) = ( Base ` C )
10	1 2 9	subcss1	|- ( ph -> S C_ ( Base ` C ) )
11	10 4	sseldd	|- ( ph -> X e. ( Base ` C ) )
12	10 5	sseldd	|- ( ph -> Y e. ( Base ` C ) )
13	6 9 3 11 12	homfval	|- ( ph -> ( X ( Homf ` C ) Y ) = ( X H Y ) )
14	8 13	sseqtrd	|- ( ph -> ( X J Y ) C_ ( X H Y ) )