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 = ( oppCat ` C )
Assertion oppccat 
|- ( C e. Cat -> O e. Cat )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 1 oppccatid 
 |-  ( C e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) )
3 2 simpld 
 |-  ( C e. Cat -> O e. Cat )