ffthoppc

Description: The opposite functor of a fully faithful functor is also full and faithful. (Contributed by Mario Carneiro, 27-Jan-2017)

	Ref	Expression
Hypotheses	fulloppc.o	$⊢ O = oppCat (C)$
	fulloppc.p	$⊢ P = oppCat (D)$
	ffthoppc.f	$⊢ φ \to F ((C Full D) \cap (C Faith D)) G$
Assertion	ffthoppc	$⊢ φ \to F ((O Full P) \cap (O Faith P)) tpos G$

Step	Hyp	Ref	Expression
1		fulloppc.o	$⊢ O = oppCat (C)$
2		fulloppc.p	$⊢ P = oppCat (D)$
3		ffthoppc.f	$⊢ φ \to F ((C Full D) \cap (C Faith D)) G$
4		brin	$⊢ F ((C Full D) \cap (C Faith D)) G \leftrightarrow (F (C Full D) G \land F (C Faith D) G)$
5	3 4	sylib	$⊢ φ \to (F (C Full D) G \land F (C Faith D) G)$
6	5	simpld	$⊢ φ \to F (C Full D) G$
7	1 2 6	fulloppc	$⊢ φ \to F (O Full P) tpos G$
8	5	simprd	$⊢ φ \to F (C Faith D) G$
9	1 2 8	fthoppc	$⊢ φ \to F (O Faith P) tpos G$
10		brin	$⊢ F ((O Full P) \cap (O Faith P)) tpos G \leftrightarrow (F (O Full P) tpos G \land F (O Faith P) tpos G)$
11	7 9 10	sylanbrc	$⊢ φ \to F ((O Full P) \cap (O Faith P)) tpos G$

Metamath Proof Explorer