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 ) |
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 ) |