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

Metamath Proof Explorer

Theorem termcnex

Description: The class of all terminal categories is a proper class. Therefore both the class of all thin categories and the class of all categories are proper classes. Note that snnex is equivalent to snglV e/ V . (Contributed by Zhi Wang, 20-Oct-2025)

		Ref	Expression
	Assertion	termcnex	⊢ TermCat ∉ V

Proof

Step	Hyp	Ref	Expression
1		snnex	⊢ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } } ∉ V
2		basrestermcfo	⊢ ( Base ↾ TermCat ) : TermCat –onto→ { 𝑏 ∣ ∃ 𝑥 𝑏 = { 𝑥 } }
3	1 2	fonex	⊢ TermCat ∉ V