Metamath Proof Explorer

Theorem 1finon

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

Ref Expression
Assertion 1finon 
|- 1o e. ( On i^i Fin )

Proof

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