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

Metamath Proof Explorer

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