Metamath Proof Explorer

Theorem onsle

Description: Less-than or equal is the same as non-strict birthday comparison over surreal ordinals. (Contributed by Scott Fenton, 25-Feb-2026)

Ref Expression
Assertion onsle 
|- ( ( A e. On_s /\ B e. On_s ) -> ( A <_s B <-> ( bday ` A ) C_ ( bday ` B ) ) )

Proof

Step Hyp Ref Expression
1 onslt 
 |-  ( ( B e. On_s /\ A e. On_s ) -> ( B  ( bday ` B ) e. ( bday ` A ) ) )
2 1 ancoms 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( B  ( bday ` B ) e. ( bday ` A ) ) )
3 2 notbid 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( -. B  -. ( bday ` B ) e. ( bday ` A ) ) )
4 onsno 
 |-  ( A e. On_s -> A e. No )
5 onsno 
 |-  ( B e. On_s -> B e. No )
6 slenlt 
 |-  ( ( A e. No /\ B e. No ) -> ( A <_s B <-> -. B
7 4 5 6 syl2an 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A <_s B <-> -. B
8 bdayelon 
 |-  ( bday ` A ) e. On
9 bdayelon 
 |-  ( bday ` B ) e. On
10 ontri1 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` A ) C_ ( bday ` B ) <-> -. ( bday ` B ) e. ( bday ` A ) ) )
11 8 9 10 mp2an 
 |-  ( ( bday ` A ) C_ ( bday ` B ) <-> -. ( bday ` B ) e. ( bday ` A ) )
12 11 a1i 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( ( bday ` A ) C_ ( bday ` B ) <-> -. ( bday ` B ) e. ( bday ` A ) ) )
13 3 7 12 3bitr4d 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( A <_s B <-> ( bday ` A ) C_ ( bday ` B ) ) )