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

Metamath Proof Explorer

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 )