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↾catJ
rescfth.i ⊢I=idfunc⁡D
Assertion rescfth ⊢J∈Subcat⁡C→I∈DFaithC

Proof

Step Hyp Ref Expression
1 rescfth.d ⊢D=C↾catJ
2 rescfth.i ⊢I=idfunc⁡D
3 1 oveq2i ⊢DFaithD=DFaithC↾catJ
4 fthres2 ⊢J∈Subcat⁡C→DFaithC↾catJ⊆DFaithC
5 3 4 eqsstrid ⊢J∈Subcat⁡C→DFaithD⊆DFaithC
6 id ⊢J∈Subcat⁡C→J∈Subcat⁡C
7 1 6 subccat ⊢J∈Subcat⁡C→D∈Cat
8 2 idffth ⊢D∈Cat→I∈DFullD∩DFaithD
9 7 8 syl ⊢J∈Subcat⁡C→I∈DFullD∩DFaithD
10 9 elin2d ⊢J∈Subcat⁡C→I∈DFaithD
11 5 10 sseldd ⊢J∈Subcat⁡C→I∈DFaithC