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	Could not format assertion : No typesetting found for |- TermCat e/ _V with typecode |-

Proof

Step	Hyp	Ref	Expression
1		snnex	$$⊢\left\{b|\exists xb=\left\{x\right\}\right\}\notin \mathrm{V}$$
2		basrestermcfo	Could not format ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } : No typesetting found for |- ( Base |` TermCat ) : TermCat -onto-> { b | E. x b = { x } } with typecode |-
3	1 2	fonex	Could not format TermCat e/ _V : No typesetting found for |- TermCat e/ _V with typecode |-