Metamath Proof Explorer

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 
|- ( -. _om e. _V <-> _om = On )

Proof

Step Hyp Ref Expression
1 fineqv 
 |-  ( -. _om e. _V <-> Fin = _V )
2 fineqvomonb 
 |-  ( Fin = _V <-> _om = On )
3 1 2 bitri 
 |-  ( -. _om e. _V <-> _om = On )