Metamath Proof Explorer


Theorem 2oppcbas

Description: The double opposite category has the same objects as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses oppcbas.1 O = oppCat C
2oppcco.2 B = Base C
Assertion 2oppcbas B = Base oppCat O

Proof

Step Hyp Ref Expression
1 oppcbas.1 O = oppCat C
2 2oppcco.2 B = Base C
3 eqid oppCat O = oppCat O
4 1 2 oppcbas B = Base O
5 3 4 oppcbas B = Base oppCat O