Metamath Proof Explorer


Theorem oppccat

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

Ref Expression
Hypothesis oppcbas.1 𝑂 = ( oppCat ‘ 𝐶 )
Assertion oppccat ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )

Proof

Step Hyp Ref Expression
1 oppcbas.1 𝑂 = ( oppCat ‘ 𝐶 )
2 1 oppccatid ( 𝐶 ∈ Cat → ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ) )
3 2 simpld ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )