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	⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
	rescfth.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
Assertion	rescfth	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 ∈ ( 𝐷 Faith 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rescfth.d	⊢ 𝐷 = ( 𝐶 ↾cat 𝐽 )
2		rescfth.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
3	1	oveq2i	⊢ ( 𝐷 Faith 𝐷 ) = ( 𝐷 Faith ( 𝐶 ↾cat 𝐽 ) )
4		fthres2	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐷 Faith ( 𝐶 ↾cat 𝐽 ) ) ⊆ ( 𝐷 Faith 𝐶 ) )
5	3 4	eqsstrid	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → ( 𝐷 Faith 𝐷 ) ⊆ ( 𝐷 Faith 𝐶 ) )
6		id	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
7	1 6	subccat	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐷 ∈ Cat )
8	2	idffth	⊢ ( 𝐷 ∈ Cat → 𝐼 ∈ ( ( 𝐷 Full 𝐷 ) ∩ ( 𝐷 Faith 𝐷 ) ) )
9	7 8	syl	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 ∈ ( ( 𝐷 Full 𝐷 ) ∩ ( 𝐷 Faith 𝐷 ) ) )
10	9	elin2d	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 ∈ ( 𝐷 Faith 𝐷 ) )
11	5 10	sseldd	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐼 ∈ ( 𝐷 Faith 𝐶 ) )