Theorem fthres2

Description: A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Assertion	fthres2	|- ( R e. ( Subcat ` D ) -> ( C Faith ( D |`cat R ) ) C_ ( C Faith D ) )

Proof

Step	Hyp	Ref	Expression
1		relfth	|- Rel ( C Faith ( D |`cat R ) )
2	1	a1i	|- ( R e. ( Subcat ` D ) -> Rel ( C Faith ( D |`cat R ) ) )
3		funcres2	|- ( R e. ( Subcat ` D ) -> ( C Func ( D |`cat R ) ) C_ ( C Func D ) )
4	3	ssbrd	|- ( R e. ( Subcat ` D ) -> ( f ( C Func ( D |`cat R ) ) g -> f ( C Func D ) g ) )
5	4	anim1d	|- ( R e. ( Subcat ` D ) -> ( ( f ( C Func ( D |`cat R ) ) g /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x g y ) ) -> ( f ( C Func D ) g /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x g y ) ) ) )
6		eqid	|- ( Base ` C ) = ( Base ` C )
7	6	isfth	|- ( f ( C Faith ( D |`cat R ) ) g <-> ( f ( C Func ( D |`cat R ) ) g /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x g y ) ) )
8	6	isfth	|- ( f ( C Faith D ) g <-> ( f ( C Func D ) g /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) Fun `' ( x g y ) ) )
9	5 7 8	3imtr4g	|- ( R e. ( Subcat ` D ) -> ( f ( C Faith ( D |`cat R ) ) g -> f ( C Faith D ) g ) )
10		df-br	|- ( f ( C Faith ( D |`cat R ) ) g <-> <. f , g >. e. ( C Faith ( D |`cat R ) ) )
11		df-br	|- ( f ( C Faith D ) g <-> <. f , g >. e. ( C Faith D ) )
12	9 10 11	3imtr3g	|- ( R e. ( Subcat ` D ) -> ( <. f , g >. e. ( C Faith ( D |`cat R ) ) -> <. f , g >. e. ( C Faith D ) ) )
13	2 12	relssdv	|- ( R e. ( Subcat ` D ) -> ( C Faith ( D |`cat R ) ) C_ ( C Faith D ) )