Theorem subcss1

Description: The objects of a subcategory are a subset of the objects 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 ) )
	subcss1.b	|- B = ( Base ` C )
Assertion	subcss1	|- ( ph -> S C_ B )

Proof

Step	Hyp	Ref	Expression
1		subcss1.1	|- ( ph -> J e. ( Subcat ` C ) )
2		subcss1.2	|- ( ph -> J Fn ( S X. S ) )
3		subcss1.b	|- B = ( Base ` C )
4		eqid	|- ( Homf ` C ) = ( Homf ` C )
5	4 3	homffn	|- ( Homf ` C ) Fn ( B X. B )
6	5	a1i	|- ( ph -> ( Homf ` C ) Fn ( B X. B ) )
7	1 4	subcssc	|- ( ph -> J C_cat ( Homf ` C ) )
8	2 6 7	ssc1	|- ( ph -> S C_ B )