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 φ F C Full D C Faith D G
Assertion ffthoppc φ F O Full P 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 φ F C Full D C Faith D G
4 brin F C Full D C Faith D G F C Full D G F C Faith D G
5 3 4 sylib φ F C Full D G F C Faith D G
6 5 simpld φ F C Full D G
7 1 2 6 fulloppc φ F O Full P tpos G
8 5 simprd φ F C Faith D G
9 1 2 8 fthoppc φ F O Faith P tpos G
10 brin F O Full P O Faith P tpos G F O Full P tpos G F O Faith P tpos G
11 7 9 10 sylanbrc φ F O Full P O Faith P tpos G