Metamath Proof Explorer


Theorem oppcid

Description: Identity function of an opposite category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses oppcbas.1 O = oppCat C
oppcid.2 B = Id C
Assertion oppcid C Cat Id O = B

Proof

Step Hyp Ref Expression
1 oppcbas.1 O = oppCat C
2 oppcid.2 B = Id C
3 1 oppccatid C Cat O Cat Id O = Id C
4 3 simprd C Cat Id O = Id C
5 4 2 eqtr4di C Cat Id O = B