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

Metamath Proof Explorer

Theorem fthres2

Description: A faithful functor into a restricted category is also a faithful functor into the whole category. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Assertion fthres2 ⊢ R ∈ Subcat ⁡ D → C Faith D ↾ cat R ⊆ C Faith D

Proof

Step Hyp Ref Expression
1 relfth ⊢ Rel ⁡ C Faith D ↾ cat R
2 1 a1i ⊢ R ∈ Subcat ⁡ D → Rel ⁡ C Faith D ↾ cat R
3 funcres2 ⊢ R ∈ Subcat ⁡ D → C Func D ↾ cat R ⊆ C Func D
4 3 ssbrd ⊢ R ∈ Subcat ⁡ D → f C Func D ↾ cat R g → f C Func D g
5 4 anim1d ⊢ R ∈ Subcat ⁡ D → f C Func D ↾ cat R g ∧ ∀ x ∈ Base C ∀ y ∈ Base C Fun ⁡ x g y -1 → f C Func D g ∧ ∀ x ∈ Base C ∀ y ∈ Base C Fun ⁡ x g y -1
6 eqid ⊢ Base C = Base C
7 6 isfth ⊢ f C Faith D ↾ cat R g ↔ f C Func D ↾ cat R g ∧ ∀ x ∈ Base C ∀ y ∈ Base C Fun ⁡ x g y -1
8 6 isfth ⊢ f C Faith D g ↔ f C Func D g ∧ ∀ x ∈ Base C ∀ y ∈ Base C Fun ⁡ x g y -1
9 5 7 8 3imtr4g ⊢ R ∈ Subcat ⁡ D → f C Faith D ↾ cat R g → f C Faith D g
10 df-br ⊢ f C Faith D ↾ cat R g ↔ f g ∈ C Faith D ↾ cat R
11 df-br ⊢ f C Faith D g ↔ f g ∈ C Faith D
12 9 10 11 3imtr3g ⊢ R ∈ Subcat ⁡ D → f g ∈ C Faith D ↾ cat R → f g ∈ C Faith D
13 2 12 relssdv ⊢ R ∈ Subcat ⁡ D → C Faith D ↾ cat R ⊆ C Faith D