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	⊢ ( ¬ ω ∈ V ↔ ω = On )

Proof

Step	Hyp	Ref	Expression
1		fineqv	⊢ ( ¬ ω ∈ V ↔ Fin = V )
2		fineqvomonb	⊢ ( Fin = V ↔ ω = On )
3	1 2	bitri	⊢ ( ¬ ω ∈ V ↔ ω = On )