Metamath Proof Explorer

Theorem 4no

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

Ref Expression
Assertion 4no 
|- ( 4o X. { 2o } ) e. No

Proof

Step Hyp Ref Expression
1 4on 
 |-  4o e. On
2 1 onnoi 
 |-  ( 4o X. { 2o } ) e. No