Metamath Proof Explorer

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	$⊢ φ \to B = {Base}_{C}$
		indcthing.h	$⊢ φ \to H = Hom (C)$
		indcthing.c	$⊢ φ \to C \in Cat$
		indcthing.i	$⊢ (φ \land (x \in B \land y \in B)) \to x H y = \{F\}$
	Assertion	indcthing	$⊢ φ \to C \in ThinCat$

Proof

Step	Hyp	Ref	Expression
1		indcthing.b	$⊢ φ \to B = {Base}_{C}$
2		indcthing.h	$⊢ φ \to H = Hom (C)$
3		indcthing.c	$⊢ φ \to C \in Cat$
4		indcthing.i	$⊢ (φ \land (x \in B \land y \in B)) \to x H y = \{F\}$
5		eqid	$⊢ \{F\} = \{F\}$
6		mosn	$⊢ \{F\} = \{F\} \to \exists^{*} f f \in \{F\}$
7	5 6	ax-mp	$⊢ \exists^{*} f f \in \{F\}$
8	4	eleq2d	$⊢ (φ \land (x \in B \land y \in B)) \to (f \in (x H y) \leftrightarrow f \in \{F\})$
9	8	mobidv	$⊢ (φ \land (x \in B \land y \in B)) \to (\exists^{} f f \in (x H y) \leftrightarrow \exists^{} f f \in \{F\})$
10	7 9	mpbiri	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x H y)$
11	1 2 10 3	isthincd	$⊢ φ \to C \in ThinCat$