Metamath Proof Explorer


Theorem oppccat

Description: An opposite category is a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 O=oppCatC
Assertion oppccat CCatOCat

Proof

Step Hyp Ref Expression
1 oppcbas.1 O=oppCatC
2 1 oppccatid CCatOCatIdO=IdC
3 2 simpld CCatOCat