Metamath Proof Explorer

Theorem 2finon

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

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

Proof

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