Metamath Proof Explorer

Theorem oppccic

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

Ref Expression
Hypotheses oppccic.o 
|- O = ( oppCat ` C )
oppccic.i 
|- ( ph -> R ( ~=c ` C ) S )
Assertion oppccic 
|- ( ph -> R ( ~=c ` O ) S )

Proof

Step Hyp Ref Expression
1 oppccic.o 
 |-  O = ( oppCat ` C )
2 oppccic.i 
 |-  ( ph -> R ( ~=c ` C ) S )
3 cicrcl2 
 |-  ( R ( ~=c ` C ) S -> C e. Cat )
4 2 3 syl 
 |-  ( ph -> C e. Cat )
5 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
6 4 5 syl 
 |-  ( ph -> O e. Cat )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 cicrcl 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> S e. ( Base ` C ) )
9 4 2 8 syl2anc 
 |-  ( ph -> S e. ( Base ` C ) )
10 ciclcl 
 |-  ( ( C e. Cat /\ R ( ~=c ` C ) S ) -> R e. ( Base ` C ) )
11 4 2 10 syl2anc 
 |-  ( ph -> R e. ( Base ` C ) )
12 eqid 
 |-  ( Iso ` C ) = ( Iso ` C )
13 eqid 
 |-  ( Iso ` O ) = ( Iso ` O )
14 7 1 4 9 11 12 13 oppciso 
 |-  ( ph -> ( S ( Iso ` O ) R ) = ( R ( Iso ` C ) S ) )
15 14 neeq1d 
 |-  ( ph -> ( ( S ( Iso ` O ) R ) =/= (/) <-> ( R ( Iso ` C ) S ) =/= (/) ) )
16 1 7 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
17 13 16 6 9 11 brcic 
 |-  ( ph -> ( S ( ~=c ` O ) R <-> ( S ( Iso ` O ) R ) =/= (/) ) )
18 12 7 4 11 9 brcic 
 |-  ( ph -> ( R ( ~=c ` C ) S <-> ( R ( Iso ` C ) S ) =/= (/) ) )
19 15 17 18 3bitr4rd 
 |-  ( ph -> ( R ( ~=c ` C ) S <-> S ( ~=c ` O ) R ) )
20 2 19 mpbid 
 |-  ( ph -> S ( ~=c ` O ) R )
21 cicsym 
 |-  ( ( O e. Cat /\ S ( ~=c ` O ) R ) -> R ( ~=c ` O ) S )
22 6 20 21 syl2anc 
 |-  ( ph -> R ( ~=c ` O ) S )