Theorem omprcomonb

Description: The class of all finite ordinals is a proper class iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026)

	Ref	Expression
Assertion	omprcomonb	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{\omega }=\mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		fineqv	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{Fin}=\mathrm{V}$$
2		fineqvomonb	$$⊢\mathrm{Fin}=\mathrm{V}\leftrightarrow \mathrm{\omega }=\mathrm{On}$$
3	1 2	bitri	$$⊢\neg \mathrm{\omega }\in \mathrm{V}\leftrightarrow \mathrm{\omega }=\mathrm{On}$$