Metamath Proof Explorer

Theorem oppccatb

Description: An opposite category is a category. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Hypotheses oppccatb.o 
|- O = ( oppCat ` C )
oppccatb.c 
|- ( ph -> C e. V )
Assertion oppccatb 
|- ( ph -> ( C e. Cat <-> O e. Cat ) )

Proof

Step Hyp Ref Expression
1 oppccatb.o 
 |-  O = ( oppCat ` C )
2 oppccatb.c 
 |-  ( ph -> C e. V )
3 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
4 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
5 4 oppccat 
 |-  ( O e. Cat -> ( oppCat ` O ) e. Cat )
6 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
7 6 a1i 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
8 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
9 8 a1i 
 |-  ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
10 fvexd 
 |-  ( ph -> ( oppCat ` O ) e. _V )
11 7 9 2 10 catpropd 
 |-  ( ph -> ( C e. Cat <-> ( oppCat ` O ) e. Cat ) )
12 5 11 imbitrrid 
 |-  ( ph -> ( O e. Cat -> C e. Cat ) )
13 3 12 impbid2 
 |-  ( ph -> ( C e. Cat <-> O e. Cat ) )