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

Metamath Proof Explorer

Theorem ffthres2c

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

		Ref	Expression
	Hypotheses	ffthres2c.a	$⊢ A = {Base}_{C}$
		ffthres2c.e	$⊢ E = D ↾_{𝑠} S$
		ffthres2c.d	$⊢ φ \to D \in Cat$
		ffthres2c.r	$⊢ φ \to S \in V$
		ffthres2c.1	$⊢ φ \to F : A ⟶ S$
	Assertion	ffthres2c	$⊢ φ \to (F ((C Full D) \cap (C Faith D)) G \leftrightarrow F ((C Full E) \cap (C Faith E)) G)$

Proof

Step	Hyp	Ref	Expression
1		ffthres2c.a	$⊢ A = {Base}_{C}$
2		ffthres2c.e	$⊢ E = D ↾_{𝑠} S$
3		ffthres2c.d	$⊢ φ \to D \in Cat$
4		ffthres2c.r	$⊢ φ \to S \in V$
5		ffthres2c.1	$⊢ φ \to F : A ⟶ S$
6	1 2 3 4 5	fullres2c	$⊢ φ \to (F (C Full D) G \leftrightarrow F (C Full E) G)$
7	1 2 3 4 5	fthres2c	$⊢ φ \to (F (C Faith D) G \leftrightarrow F (C Faith E) G)$
8	6 7	anbi12d	$⊢ φ \to ((F (C Full D) G \land F (C Faith D) G) \leftrightarrow (F (C Full E) G \land F (C Faith E) G))$
9		brin	$⊢ F ((C Full D) \cap (C Faith D)) G \leftrightarrow (F (C Full D) G \land F (C Faith D) G)$
10		brin	$⊢ F ((C Full E) \cap (C Faith E)) G \leftrightarrow (F (C Full E) G \land F (C Faith E) G)$
11	8 9 10	3bitr4g	$⊢ φ \to (F ((C Full D) \cap (C Faith D)) G \leftrightarrow F ((C Full E) \cap (C Faith E)) G)$