Theorem discthing

Description: A discrete category, i.e., a category where all morphisms are identity morphisms, is thin. Example 3.26(1) of Adamek p. 33. (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 )
	discthing.i	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = if ( x = y , { I } , (/) ) )
Assertion	discthing	|- ( 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		discthing.i	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x H y ) = if ( x = y , { I } , (/) ) )
5		eleq2w2	|- ( { I } = if ( x = y , { I } , (/) ) -> ( i e. { I } <-> i e. if ( x = y , { I } , (/) ) ) )
6	5	mobidv	|- ( { I } = if ( x = y , { I } , (/) ) -> ( E* i i e. { I } <-> E* i i e. if ( x = y , { I } , (/) ) ) )
7		eleq2w2	|- ( (/) = if ( x = y , { I } , (/) ) -> ( i e. (/) <-> i e. if ( x = y , { I } , (/) ) ) )
8	7	mobidv	|- ( (/) = if ( x = y , { I } , (/) ) -> ( E* i i e. (/) <-> E* i i e. if ( x = y , { I } , (/) ) ) )
9		eqid	|- { I } = { I }
10		mosn	|- ( { I } = { I } -> E* i i e. { I } )
11	9 10	mp1i	|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ x = y ) -> E* i i e. { I } )
12		eqid	|- (/) = (/)
13		mo0	|- ( (/) = (/) -> E* i i e. (/) )
14	12 13	mp1i	|- ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ -. x = y ) -> E* i i e. (/) )
15	6 8 11 14	ifbothda	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* i i e. if ( x = y , { I } , (/) ) )
16	4	eleq2d	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( i e. ( x H y ) <-> i e. if ( x = y , { I } , (/) ) ) )
17	16	mobidv	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( E* i i e. ( x H y ) <-> E* i i e. if ( x = y , { I } , (/) ) ) )
18	15 17	mpbird	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> E* i i e. ( x H y ) )
19	1 2 18 3	isthincd	|- ( ph -> C e. ThinCat )