Metamath Proof Explorer

Theorem 4fno

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

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

Proof

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