Metamath Proof Explorer

Theorem onsbnd2

Description: The surreals of a given birthday are bounded below by the negative of that ordinal. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Assertion onsbnd2 
|- ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` A ) <_s B )

Proof

Step Hyp Ref Expression
1 madessno 
 |-  ( _Made ` ( bday ` A ) ) C_ No
2 1 sseli 
 |-  ( B e. ( _Made ` ( bday ` A ) ) -> B e. No )
3 2 adantl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> B e. No )
4 negsbday 
 |-  ( B e. No -> ( bday ` ( -us ` B ) ) = ( bday ` B ) )
5 3 4 syl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` ( -us ` B ) ) = ( bday ` B ) )
6 madebdayim 
 |-  ( B e. ( _Made ` ( bday ` A ) ) -> ( bday ` B ) C_ ( bday ` A ) )
7 6 adantl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` B ) C_ ( bday ` A ) )
8 5 7 eqsstrd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) )
9 bdayelon 
 |-  ( bday ` A ) e. On
10 3 negscld 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) e. No )
11 madebday 
 |-  ( ( ( bday ` A ) e. On /\ ( -us ` B ) e. No ) -> ( ( -us ` B ) e. ( _Made ` ( bday ` A ) ) <-> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) ) )
12 9 10 11 sylancr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) e. ( _Made ` ( bday ` A ) ) <-> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) ) )
13 8 12 mpbird 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) e. ( _Made ` ( bday ` A ) ) )
14 onsbnd 
 |-  ( ( A e. On_s /\ ( -us ` B ) e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) <_s A )
15 13 14 syldan 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) <_s A )
16 onsno 
 |-  ( A e. On_s -> A e. No )
17 16 adantr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A e. No )
18 17 negscld 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` A ) e. No )
19 18 3 slenegd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` A ) <_s B <-> ( -us ` B ) <_s ( -us ` ( -us ` A ) ) ) )
20 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
21 17 20 syl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` ( -us ` A ) ) = A )
22 21 breq2d 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) <_s ( -us ` ( -us ` A ) ) <-> ( -us ` B ) <_s A ) )
23 19 22 bitr2d 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) <_s A <-> ( -us ` A ) <_s B ) )
24 15 23 mpbid 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` A ) <_s B )