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

Proof

Step	Hyp	Ref	Expression
1		indcthing.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2		indcthing.h	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3		indcthing.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		indcthing.i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = { 𝐹 } )
5		eqid	⊢ { 𝐹 } = { 𝐹 }
6		mosn	⊢ ( { 𝐹 } = { 𝐹 } → ∃* 𝑓 𝑓 ∈ { 𝐹 } )
7	5 6	ax-mp	⊢ ∃* 𝑓 𝑓 ∈ { 𝐹 }
8	4	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ { 𝐹 } ) )
9	8	mobidv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ { 𝐹 } ) )
10	7 9	mpbiri	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
11	1 2 10 3	isthincd	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )