Metamath Proof Explorer

Theorem fthres2c

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

Ref Expression
Hypotheses fthres2c.a ⊢ A = Base C
fthres2c.e ⊢ E = D ↾ 𝑠 S
fthres2c.d ⊢ φ → D ∈ Cat
fthres2c.r ⊢ φ → S ∈ V
fthres2c.1 ⊢ φ → F : A ⟶ S
Assertion fthres2c ⊢ φ → F C Faith D G ↔ F C Faith E G

Proof

Step Hyp Ref Expression
1 fthres2c.a ⊢ A = Base C
2 fthres2c.e ⊢ E = D ↾ 𝑠 S
3 fthres2c.d ⊢ φ → D ∈ Cat
4 fthres2c.r ⊢ φ → S ∈ V
5 fthres2c.1 ⊢ φ → F : A ⟶ S
6 1 2 3 4 5 funcres2c ⊢ φ → F C Func D G ↔ F C Func E G
7 6 anbi1d ⊢ φ → F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1 ↔ F C Func E G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
8 1 isfth ⊢ F C Faith D G ↔ F C Func D G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
9 1 isfth ⊢ F C Faith E G ↔ F C Func E G ∧ ∀ x ∈ A ∀ y ∈ A Fun ⁡ x G y -1
10 7 8 9 3bitr4g ⊢ φ → F C Faith D G ↔ F C Faith E G