Metamath Proof Explorer

Theorem onswe

Description: Surreal less-than well-orders the surreal ordinals. Part of Theorem 15 of Conway p. 28. (Contributed by Scott Fenton, 6-Nov-2025)

Ref Expression
Assertion onswe 
|-

Proof

Step Hyp Ref Expression
1 epweon 
 |-  _E We On
2 onsiso 
 |-  ( bday |` On_s ) Isom
3 isowe 
 |-  ( ( bday |` On_s ) Isom  (  _E We On ) )
4 2 3 ax-mp 
 |-  (  _E We On )
5 1 4 mpbir 
 |-