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	$⊢ φ \to R \in Subcat (D)$
	fthres2b.s	$⊢ φ \to R Fn (S \times S)$
	fthres2b.1	$⊢ φ \to F : A ⟶ S$
	fthres2b.2	$⊢ (φ \land (x \in A \land y \in A)) \to (x G y) : Y ⟶ F (x) R F (y)$
Assertion	fthres2b	$⊢ φ \to (F (C Faith D) G \leftrightarrow F (C Faith (D ↾_{cat} R)) G)$

Step	Hyp	Ref	Expression
1		fthres2b.a	$⊢ A = {Base}_{C}$
2		fthres2b.h	$⊢ H = Hom (C)$
3		fthres2b.r	$⊢ φ \to R \in Subcat (D)$
4		fthres2b.s	$⊢ φ \to R Fn (S \times S)$
5		fthres2b.1	$⊢ φ \to F : A ⟶ S$
6		fthres2b.2	$⊢ (φ \land (x \in A \land y \in A)) \to (x G y) : Y ⟶ F (x) R F (y)$
7	1 2 3 4 5 6	funcres2b	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func (D ↾_{cat} R)) G)$
8	7	anbi1d	$⊢ φ \to ((F (C Func D) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1}) \leftrightarrow (F (C Func (D ↾_{cat} R)) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1}))$
9	1	isfth	$⊢ F (C Faith D) G \leftrightarrow (F (C Func D) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1})$
10	1	isfth	$⊢ F (C Faith (D ↾_{cat} R)) G \leftrightarrow (F (C Func (D ↾_{cat} R)) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1})$
11	8 9 10	3bitr4g	$⊢ φ \to (F (C Faith D) G \leftrightarrow F (C Faith (D ↾_{cat} R)) G)$

Metamath Proof Explorer