This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )