Metamath Proof Explorer

Theorem 0finon

Description: 0 is a finite ordinal. See peano1 . (Contributed by RP, 27-Sep-2023)

Ref Expression
Assertion 0finon 
|- (/) e. ( On i^i Fin )

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 onfin2 
 |-  _om = ( On i^i Fin )
3 1 2 eleqtri 
 |-  (/) e. ( On i^i Fin )