Metamath Proof Explorer

Theorem onno

Description: Every ordinal maps to a surreal number. (Contributed by RP, 21-Sep-2023)

Ref Expression
Assertion onno 
|- ( A e. On -> ( A X. { 2o } ) e. No )

Proof

Step Hyp Ref Expression
1 2oex 
 |-  2o e. _V
2 1 prid2 
 |-  2o e. { 1o , 2o }
3 onnog 
 |-  ( ( A e. On /\ 2o e. { 1o , 2o } ) -> ( A X. { 2o } ) e. No )
4 2 3 mpan2 
 |-  ( A e. On -> ( A X. { 2o } ) e. No )