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 ⊢ 𝐷 = ( 𝐶 ↾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 𝐶 ) )