Metamath Proof Explorer


Theorem oppcid

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

Ref Expression
Hypotheses oppcbas.1 𝑂 = ( oppCat ‘ 𝐶 )
oppcid.2 𝐵 = ( Id ‘ 𝐶 )
Assertion oppcid ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 oppcbas.1 𝑂 = ( oppCat ‘ 𝐶 )
2 oppcid.2 𝐵 = ( Id ‘ 𝐶 )
3 1 oppccatid ( 𝐶 ∈ Cat → ( 𝑂 ∈ Cat ∧ ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) ) )
4 3 simprd ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = ( Id ‘ 𝐶 ) )
5 4 2 eqtr4di ( 𝐶 ∈ Cat → ( Id ‘ 𝑂 ) = 𝐵 )