Theorem rescfth

Description: The inclusion functor from a subcategory is a faithful functor. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	rescfth.d	|- D = ( C |`cat J )
	rescfth.i	|- I = ( idFunc ` D )
Assertion	rescfth	|- ( J e. ( Subcat ` C ) -> I e. ( D Faith C ) )

Proof

Step	Hyp	Ref	Expression
1		rescfth.d	|- D = ( C |`cat J )
2		rescfth.i	|- I = ( idFunc ` D )
3	1	oveq2i	|- ( D Faith D ) = ( D Faith ( C |`cat J ) )
4		fthres2	|- ( J e. ( Subcat ` C ) -> ( D Faith ( C |`cat J ) ) C_ ( D Faith C ) )
5	3 4	eqsstrid	|- ( J e. ( Subcat ` C ) -> ( D Faith D ) C_ ( D Faith C ) )
6		id	|- ( J e. ( Subcat ` C ) -> J e. ( Subcat ` C ) )
7	1 6	subccat	|- ( J e. ( Subcat ` C ) -> D e. Cat )
8	2	idffth	|- ( D e. Cat -> I e. ( ( D Full D ) i^i ( D Faith D ) ) )
9	7 8	syl	|- ( J e. ( Subcat ` C ) -> I e. ( ( D Full D ) i^i ( D Faith D ) ) )
10	9	elin2d	|- ( J e. ( Subcat ` C ) -> I e. ( D Faith D ) )
11	5 10	sseldd	|- ( J e. ( Subcat ` C ) -> I e. ( D Faith C ) )