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

Metamath Proof Explorer

Theorem fthres2b

Description: Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthres2b.a ⊢ A = Base C
fthres2b.h ⊢ H = Hom ⁡ C
fthres2b.r ⊢ φ → R ∈ Subcat ⁡ D
fthres2b.s ⊢ φ → R Fn S × S
fthres2b.1 ⊢ φ → F : A ⟶ S
fthres2b.2 ⊢ φ ∧ x ∈ A ∧ y ∈ A → x G y : Y ⟶ F ⁡ x R F ⁡ y
Assertion fthres2b ⊢ φ → F C Faith D G ↔ F C Faith D ↾ cat R G

Proof

Step Hyp Ref Expression
1 fthres2b.a ⊢ A = Base C
2 fthres2b.h ⊢ H = Hom ⁡ C
3 fthres2b.r ⊢ φ → R ∈ Subcat ⁡ D
4 fthres2b.s ⊢ φ → R Fn S × S
5 fthres2b.1 ⊢ φ → F : A ⟶ S
6 fthres2b.2 ⊢ φ ∧ x ∈ A ∧ y ∈ A → x G y : Y ⟶ F ⁡ x R F ⁡ y
7 1 2 3 4 5 6 funcres2b ⊢ φ → F C Func D G ↔ F C Func D ↾ cat R G
8 7 anbi1d ⊢ φ → F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1 ↔ F C Func D ↾ cat R G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
9 1 isfth ⊢ F C Faith D G ↔ F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
10 1 isfth ⊢ F C Faith D ↾ cat R G ↔ F C Func D ↾ cat R G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
11 8 9 10 3bitr4g ⊢ φ → F C Faith D G ↔ F C Faith D ↾ cat R G