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	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	indcthing.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
	indcthing.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	discthing.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) )
Assertion	discthing	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step	Hyp	Ref	Expression
1		indcthing.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2		indcthing.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3		indcthing.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		discthing.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) )
5		eleq2w2	⊢ ( { 𝐼 } = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( 𝑖 ∈ { 𝐼 } ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
6	5	mobidv	⊢ ( { 𝐼 } = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( ∃* 𝑖 𝑖 ∈ { 𝐼 } ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
7		eleq2w2	⊢ ( ∅ = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( 𝑖 ∈ ∅ ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
8	7	mobidv	⊢ ( ∅ = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( ∃* 𝑖 𝑖 ∈ ∅ ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
9		eqid	⊢ { 𝐼 } = { 𝐼 }
10		mosn	⊢ ( { 𝐼 } = { 𝐼 } → ∃* 𝑖 𝑖 ∈ { 𝐼 } )
11	9 10	mp1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ∃* 𝑖 𝑖 ∈ { 𝐼 } )
12		eqid	⊢ ∅ = ∅
13		mo0	⊢ ( ∅ = ∅ → ∃* 𝑖 𝑖 ∈ ∅ )
14	12 13	mp1i	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ∃* 𝑖 𝑖 ∈ ∅ )
15	6 8 11 14	ifbothda	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) )
16	4	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
17	16	mobidv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃* 𝑖 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
18	15 17	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑖 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) )
19	1 2 18 3	isthincd	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )