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 \in Subcat (D) \to C Faith (D ↾_{cat} R) \subseteq C Faith D$

Proof

Step	Hyp	Ref	Expression
1		relfth	$⊢ Rel (C Faith (D ↾_{cat} R))$
2	1	a1i	$⊢ R \in Subcat (D) \to Rel (C Faith (D ↾_{cat} R))$
3		funcres2	$⊢ R \in Subcat (D) \to C Func (D ↾_{cat} R) \subseteq C Func D$
4	3	ssbrd	$⊢ R \in Subcat (D) \to (f (C Func (D ↾_{cat} R)) g \to f (C Func D) g)$
5	4	anim1d	$⊢ R \in Subcat (D) \to ((f (C Func (D ↾_{cat} R)) g \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} Fun {(x g y)}^{-1}) \to (f (C Func D) g \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} Fun {(x g y)}^{-1}))$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	6	isfth	$⊢ f (C Faith (D ↾_{cat} R)) g \leftrightarrow (f (C Func (D ↾_{cat} R)) g \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} Fun {(x g y)}^{-1})$
8	6	isfth	$⊢ f (C Faith D) g \leftrightarrow (f (C Func D) g \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} Fun {(x g y)}^{-1})$
9	5 7 8	3imtr4g	$⊢ R \in Subcat (D) \to (f (C Faith (D ↾_{cat} R)) g \to f (C Faith D) g)$
10		df-br	$⊢ f (C Faith (D ↾_{cat} R)) g \leftrightarrow ⟨f, g⟩ \in (C Faith (D ↾_{cat} R))$
11		df-br	$⊢ f (C Faith D) g \leftrightarrow ⟨f, g⟩ \in (C Faith D)$
12	9 10 11	3imtr3g	$⊢ R \in Subcat (D) \to (⟨f, g⟩ \in (C Faith (D ↾_{cat} R)) \to ⟨f, g⟩ \in (C Faith D))$
13	2 12	relssdv	$⊢ R \in Subcat (D) \to C Faith (D ↾_{cat} R) \subseteq C Faith D$