This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppcciceq

Description: The opposite category has the same isomorphic objects as the original category. (Contributed by Zhi Wang, 27-Oct-2025)

Ref Expression
Hypothesis oppccicb.o 
|- O = ( oppCat ` C )
Assertion oppcciceq 
|- ( ~=c ` C ) = ( ~=c ` O )

Proof

Step Hyp Ref Expression
1 oppccicb.o 
 |-  O = ( oppCat ` C )
2 cic1st2nd 
 |-  ( p e. ( ~=c ` C ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
3 cic1st2ndbr 
 |-  ( p e. ( ~=c ` C ) -> ( 1st ` p ) ( ~=c ` C ) ( 2nd ` p ) )
4 1 3 oppccic 
 |-  ( p e. ( ~=c ` C ) -> ( 1st ` p ) ( ~=c ` O ) ( 2nd ` p ) )
5 df-br 
 |-  ( ( 1st ` p ) ( ~=c ` O ) ( 2nd ` p ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ~=c ` O ) )
6 4 5 sylib 
 |-  ( p e. ( ~=c ` C ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ~=c ` O ) )
7 2 6 eqeltrd 
 |-  ( p e. ( ~=c ` C ) -> p e. ( ~=c ` O ) )
8 cic1st2nd 
 |-  ( p e. ( ~=c ` O ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
9 cic1st2ndbr 
 |-  ( p e. ( ~=c ` O ) -> ( 1st ` p ) ( ~=c ` O ) ( 2nd ` p ) )
10 1 oppccicb 
 |-  ( ( 1st ` p ) ( ~=c ` C ) ( 2nd ` p ) <-> ( 1st ` p ) ( ~=c ` O ) ( 2nd ` p ) )
11 9 10 sylibr 
 |-  ( p e. ( ~=c ` O ) -> ( 1st ` p ) ( ~=c ` C ) ( 2nd ` p ) )
12 df-br 
 |-  ( ( 1st ` p ) ( ~=c ` C ) ( 2nd ` p ) <-> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ~=c ` C ) )
13 11 12 sylib 
 |-  ( p e. ( ~=c ` O ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. e. ( ~=c ` C ) )
14 8 13 eqeltrd 
 |-  ( p e. ( ~=c ` O ) -> p e. ( ~=c ` C ) )
15 7 14 impbii 
 |-  ( p e. ( ~=c ` C ) <-> p e. ( ~=c ` O ) )
16 15 eqriv 
 |-  ( ~=c ` C ) = ( ~=c ` O )