This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem istermc2

Description: The predicate "is a terminal category". A terminal category is a thin category with exactly one object. (Contributed by Zhi Wang, 16-Oct-2025)

		Ref	Expression
	Hypothesis	istermc.b	$⊢ B = {Base}_{C}$
	Assertion	istermc2	Could not format assertion : No typesetting found for \|- ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. B ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		istermc.b	$⊢ B = {Base}_{C}$
2	1	istermc	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) : No typesetting found for \|- ( C e. TermCat <-> ( C e. ThinCat /\ E. x B = { x } ) ) with typecode \|-
3		eusn	$⊢ \exists! x x \in B \leftrightarrow \exists x B = \{x\}$
4	3	anbi2i	$⊢ (C \in ThinCat \land \exists! x x \in B) \leftrightarrow (C \in ThinCat \land \exists x B = \{x\})$
5	2 4	bitr4i	Could not format ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. B ) ) : No typesetting found for \|- ( C e. TermCat <-> ( C e. ThinCat /\ E! x x e. B ) ) with typecode \|-