Metamath Proof Explorer

Theorem 2omomeqom

Description: Ordinal two times omega is omega. Lemma 3.17 of Schloeder p. 10. (Contributed by RP, 30-Jan-2025)

Ref Expression
Assertion 2omomeqom 
|- ( 2o .o _om ) = _om

Proof

Step Hyp Ref Expression
1 omelon 
 |-  _om e. On
2 2onn 
 |-  2o e. _om
3 0ex 
 |-  (/) e. _V
4 3 prid1 
 |-  (/) e. { (/) , { (/) } }
5 df2o2 
 |-  2o = { (/) , { (/) } }
6 4 5 eleqtrri 
 |-  (/) e. 2o
7 omabslem 
 |-  ( ( _om e. On /\ 2o e. _om /\ (/) e. 2o ) -> ( 2o .o _om ) = _om )
8 1 2 6 7 mp3an 
 |-  ( 2o .o _om ) = _om