Description: The opposite category of a thin category whose morphisms are all endomorphisms has the same base, hom-sets ( oppcendc ) and composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | oppcthinco.o | |- O = ( oppCat ` C ) |
|
| oppcthinco.c | |- ( ph -> C e. ThinCat ) |
||
| oppcthinendc.b | |- B = ( Base ` C ) |
||
| oppcthinendc.h | |- H = ( Hom ` C ) |
||
| oppcthinendc.1 | |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) ) |
||
| Assertion | oppcthinendc | |- ( ph -> ( comf ` C ) = ( comf ` O ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | oppcthinco.o | |- O = ( oppCat ` C ) |
|
| 2 | oppcthinco.c | |- ( ph -> C e. ThinCat ) |
|
| 3 | oppcthinendc.b | |- B = ( Base ` C ) |
|
| 4 | oppcthinendc.h | |- H = ( Hom ` C ) |
|
| 5 | oppcthinendc.1 | |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x =/= y -> ( x H y ) = (/) ) ) |
|
| 6 | 1 3 4 5 | oppcendc | |- ( ph -> ( Homf ` C ) = ( Homf ` O ) ) |
| 7 | 1 2 6 | oppcthinco | |- ( ph -> ( comf ` C ) = ( comf ` O ) ) |