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 e. 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 e. Cat -> ( O e. Cat /\ ( Id ` O ) = ( Id ` C ) ) )
4 3 simprd
 |-  ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
5 4 2 eqtr4di
 |-  ( C e. Cat -> ( Id ` O ) = B )