Metamath Proof Explorer

Theorem 3finon

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

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

Proof

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