Metamath Proof Explorer

Theorem fineqvomonb

Description: All sets are finite iff all ordinal sets are finite. (Contributed by BTernaryTau, 25-Jan-2026)

Ref Expression
Assertion fineqvomonb 
|- ( Fin = _V <-> _om = On )

Proof

Step Hyp Ref Expression
1 fineqvomon 
 |-  ( Fin = _V -> _om = On )
2 onprc 
 |-  -. On e. _V
3 eleq1 
 |-  ( _om = On -> ( _om e. _V <-> On e. _V ) )
4 2 3 mtbiri 
 |-  ( _om = On -> -. _om e. _V )
5 fineqv 
 |-  ( -. _om e. _V <-> Fin = _V )
6 4 5 sylib 
 |-  ( _om = On -> Fin = _V )
7 1 6 impbii 
 |-  ( Fin = _V <-> _om = On )