Theorem indcthing

Description: An indiscrete category, i.e., a category where all hom-sets have exactly one morphism, is thin. (Contributed by Zhi Wang, 11-Nov-2025)

	Ref	Expression
Hypotheses	indcthing.b	|- ( ph -> B = ( Base ` C ) )
	indcthing.h	|- ( ph -> H = ( Hom ` C ) )
	indcthing.c	|- ( ph -> C e. Cat )
	indcthing.i	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = { F } )
Assertion	indcthing	|- ( ph -> C e. ThinCat )

Proof

Step	Hyp	Ref	Expression
1		indcthing.b	|- ( ph -> B = ( Base ` C ) )
2		indcthing.h	|- ( ph -> H = ( Hom ` C ) )
3		indcthing.c	|- ( ph -> C e. Cat )
4		indcthing.i	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = { F } )
5		eqid	|- { F } = { F }
6		mosn	|- ( { F } = { F } -> E* f f e. { F } )
7	5 6	ax-mp	|- E* f f e. { F }
8	4	eleq2d	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( f e. ( x H y ) <-> f e. { F } ) )
9	8	mobidv	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E* f f e. ( x H y ) <-> E* f f e. { F } ) )
10	7 9	mpbiri	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* f f e. ( x H y ) )
11	1 2 10 3	isthincd	|- ( ph -> C e. ThinCat )