Metamath Proof Explorer

Theorem oppccicb

Description: Isomorphic objects are isomorphic in the opposite category. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypothesis oppccicb.o 
|- O = ( oppCat ` C )
Assertion oppccicb 
|- ( R ( ~=c ` C ) S <-> R ( ~=c ` O ) S )

Proof

Step Hyp Ref Expression
1 oppccicb.o 
 |-  O = ( oppCat ` C )
2 id 
 |-  ( R ( ~=c ` C ) S -> R ( ~=c ` C ) S )
3 1 2 oppccic 
 |-  ( R ( ~=c ` C ) S -> R ( ~=c ` O ) S )
4 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
5 id 
 |-  ( R ( ~=c ` O ) S -> R ( ~=c ` O ) S )
6 4 5 oppccic 
 |-  ( R ( ~=c ` O ) S -> R ( ~=c ` ( oppCat ` O ) ) S )
7 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
8 7 a1i 
 |-  ( R ( ~=c ` O ) S -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
9 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
10 9 a1i 
 |-  ( R ( ~=c ` O ) S -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
11 8 10 cicpropd 
 |-  ( R ( ~=c ` O ) S -> ( ~=c ` C ) = ( ~=c ` ( oppCat ` O ) ) )
12 11 breqd 
 |-  ( R ( ~=c ` O ) S -> ( R ( ~=c ` C ) S <-> R ( ~=c ` ( oppCat ` O ) ) S ) )
13 6 12 mpbird 
 |-  ( R ( ~=c ` O ) S -> R ( ~=c ` C ) S )
14 3 13 impbii 
 |-  ( R ( ~=c ` C ) S <-> R ( ~=c ` O ) S )