Metamath Proof Explorer

Theorem 4finon

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

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

Proof

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