Theorem 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	|- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
Assertion	ffthoppc	|- ( ph -> F ( ( O Full P ) i^i ( O Faith P ) ) tpos G )

Proof

Step	Hyp	Ref	Expression
1		fulloppc.o	|- O = ( oppCat ` C )
2		fulloppc.p	|- P = ( oppCat ` D )
3		ffthoppc.f	|- ( ph -> F ( ( C Full D ) i^i ( C Faith D ) ) G )
4		brin	|- ( F ( ( C Full D ) i^i ( C Faith D ) ) G <-> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
5	3 4	sylib	|- ( ph -> ( F ( C Full D ) G /\ F ( C Faith D ) G ) )
6	5	simpld	|- ( ph -> F ( C Full D ) G )
7	1 2 6	fulloppc	|- ( ph -> F ( O Full P ) tpos G )
8	5	simprd	|- ( ph -> F ( C Faith D ) G )
9	1 2 8	fthoppc	|- ( ph -> F ( O Faith P ) tpos G )
10		brin	|- ( F ( ( O Full P ) i^i ( O Faith P ) ) tpos G <-> ( F ( O Full P ) tpos G /\ F ( O Faith P ) tpos G ) )
11	7 9 10	sylanbrc	|- ( ph -> F ( ( O Full P ) i^i ( O Faith P ) ) tpos G )