Metamath Proof Explorer

Theorem oppcthin

Description: The opposite category of a thin category is thin. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Hypothesis oppcthin.o 
|- O = ( oppCat ` C )
Assertion oppcthin 
|- ( C e. ThinCat -> O e. ThinCat )

Proof

Step Hyp Ref Expression
1 oppcthin.o 
 |-  O = ( oppCat ` C )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 1 2 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
4 3 a1i 
 |-  ( C e. ThinCat -> ( Base ` C ) = ( Base ` O ) )
5 eqidd 
 |-  ( C e. ThinCat -> ( Hom ` O ) = ( Hom ` O ) )
6 simpl 
 |-  ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat )
7 simprr 
 |-  ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
8 simprl 
 |-  ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
9 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
10 6 7 8 2 9 thincmo 
 |-  ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( y ( Hom ` C ) x ) )
11 9 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
12 11 eleq2i 
 |-  ( f e. ( x ( Hom ` O ) y ) <-> f e. ( y ( Hom ` C ) x ) )
13 12 mobii 
 |-  ( E* f f e. ( x ( Hom ` O ) y ) <-> E* f f e. ( y ( Hom ` C ) x ) )
14 10 13 sylibr 
 |-  ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( x ( Hom ` O ) y ) )
15 thincc 
 |-  ( C e. ThinCat -> C e. Cat )
16 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
17 15 16 syl 
 |-  ( C e. ThinCat -> O e. Cat )
18 4 5 14 17 isthincd 
 |-  ( C e. ThinCat -> O e. ThinCat )