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	$⊢ φ \to D \in Cat$
	fthres2c.r	$⊢ φ \to S \in V$
	fthres2c.1	$⊢ φ \to F : A ⟶ S$
Assertion	fthres2c	$⊢ φ \to (F (C Faith D) G \leftrightarrow F (C Faith E) G)$

Step	Hyp	Ref	Expression
1		fthres2c.a	$⊢ A = {Base}_{C}$
2		fthres2c.e	$⊢ E = D ↾_{𝑠} S$
3		fthres2c.d	$⊢ φ \to D \in Cat$
4		fthres2c.r	$⊢ φ \to S \in V$
5		fthres2c.1	$⊢ φ \to F : A ⟶ S$
6	1 2 3 4 5	funcres2c	$⊢ φ \to (F (C Func D) G \leftrightarrow F (C Func E) G)$
7	6	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 E) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1}))$
8	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})$
9	1	isfth	$⊢ F (C Faith E) G \leftrightarrow (F (C Func E) G \land \forall x \in A \forall y \in A Fun {(x G y)}^{-1})$
10	7 8 9	3bitr4g	$⊢ φ \to (F (C Faith D) G \leftrightarrow F (C Faith E) G)$

Metamath Proof Explorer