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=\mathrm{oppCat}\left(C\right)$$
Assertion	oppcthin	Could not format assertion : No typesetting found for |- ( C e. ThinCat -> O e. ThinCat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oppcthin.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
3	1 2	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
4	3	a1i	Could not format ( C e. ThinCat -> ( Base ` C ) = ( Base ` O ) ) : No typesetting found for |- ( C e. ThinCat -> ( Base ` C ) = ( Base ` O ) ) with typecode |-
5		eqidd	Could not format ( C e. ThinCat -> ( Hom ` O ) = ( Hom ` O ) ) : No typesetting found for |- ( C e. ThinCat -> ( Hom ` O ) = ( Hom ` O ) ) with typecode |-
6		simpl	Could not format ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> C e. ThinCat ) with typecode |-
7		simprr	Could not format ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) ) : No typesetting found for |- ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) ) with typecode |-
8		simprl	Could not format ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) ) : No typesetting found for |- ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) ) with typecode |-
9		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
10	6 7 8 2 9	thincmo	Could not format ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( y ( Hom ` C ) x ) ) : No typesetting found for |- ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( y ( Hom ` C ) x ) ) with typecode |-
11	9 1	oppchom	$$⊢x\mathrm{Hom}\left(O\right)y=y\mathrm{Hom}\left(C\right)x$$
12	11	eleq2i	$$⊢f\in \left(x\mathrm{Hom}\left(O\right)y\right)\leftrightarrow f\in \left(y\mathrm{Hom}\left(C\right)x\right)$$
13	12	mobii	$$⊢{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(O\right)y\right)\leftrightarrow {\exists }^{*}ff\in \left(y\mathrm{Hom}\left(C\right)x\right)$$
14	10 13	sylibr	Could not format ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( x ( Hom ` O ) y ) ) : No typesetting found for |- ( ( C e. ThinCat /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> E* f f e. ( x ( Hom ` O ) y ) ) with typecode |-
15		thincc	Could not format ( C e. ThinCat -> C e. Cat ) : No typesetting found for |- ( C e. ThinCat -> C e. Cat ) with typecode |-
16	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
17	15 16	syl	Could not format ( C e. ThinCat -> O e. Cat ) : No typesetting found for |- ( C e. ThinCat -> O e. Cat ) with typecode |-
18	4 5 14 17	isthincd	Could not format ( C e. ThinCat -> O e. ThinCat ) : No typesetting found for |- ( C e. ThinCat -> O e. ThinCat ) with typecode |-