Theorem 0thincg

Description: Any structure with an empty set of objects is a thin category. (Contributed by Zhi Wang, 17-Sep-2024)

	Ref	Expression
Assertion	0thincg	Could not format assertion : No typesetting found for |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0catg	$$⊢\left(C\in V\wedge \varnothing ={\mathrm{Base}}_C\right)\to C\in \mathrm{Cat}$$
2		ral0	$$⊢\forall x\in \varnothing \forall y\in {\mathrm{Base}}_C{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)$$
3		raleq	$$⊢\varnothing ={\mathrm{Base}}_C\to \left(\forall x\in \varnothing \forall y\in {\mathrm{Base}}_C{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)\leftrightarrow \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)\right)$$
4	2 3	mpbii	$$⊢\varnothing ={\mathrm{Base}}_C\to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)$$
5	4	adantl	$$⊢\left(C\in V\wedge \varnothing ={\mathrm{Base}}_C\right)\to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_C{\exists }^{*}ff\in \left(x\mathrm{Hom}\left(C\right)y\right)$$
6		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
7		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
8	6 7	isthinc	Could not format ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) : No typesetting found for |- ( C e. ThinCat <-> ( C e. Cat /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) E* f f e. ( x ( Hom ` C ) y ) ) ) with typecode |-
9	1 5 8	sylanbrc	Could not format ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( C e. V /\ (/) = ( Base ` C ) ) -> C e. ThinCat ) with typecode |-