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 = id func ⁡ D
Assertion rescfth ⊢ J ∈ Subcat ⁡ C → I ∈ D Faith C

Proof

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