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 madeno 
 |-  ( B e. ( _Made ` ( bday ` A ) ) -> B e. No )
2 1 adantl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> B e. No )
3 negbday 
 |-  ( B e. No -> ( bday ` ( -us ` B ) ) = ( bday ` B ) )
4 2 3 syl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` ( -us ` B ) ) = ( bday ` B ) )
5 madebdayim 
 |-  ( B e. ( _Made ` ( bday ` A ) ) -> ( bday ` B ) C_ ( bday ` A ) )
6 5 adantl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` B ) C_ ( bday ` A ) )
7 4 6 eqsstrd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) )
8 bdayon 
 |-  ( bday ` A ) e. On
9 2 negscld 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) e. No )
10 madebday 
 |-  ( ( ( bday ` A ) e. On /\ ( -us ` B ) e. No ) -> ( ( -us ` B ) e. ( _Made ` ( bday ` A ) ) <-> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) ) )
11 8 9 10 sylancr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) e. ( _Made ` ( bday ` A ) ) <-> ( bday ` ( -us ` B ) ) C_ ( bday ` A ) ) )
12 7 11 mpbird 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) e. ( _Made ` ( bday ` A ) ) )
13 onsbnd 
 |-  ( ( A e. On_s /\ ( -us ` B ) e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) <_s A )
14 12 13 syldan 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` B ) <_s A )
15 onno 
 |-  ( A e. On_s -> A e. No )
16 15 adantr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A e. No )
17 16 negscld 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` A ) e. No )
18 17 2 lenegsd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` A ) <_s B <-> ( -us ` B ) <_s ( -us ` ( -us ` A ) ) ) )
19 negnegs 
 |-  ( A e. No -> ( -us ` ( -us ` A ) ) = A )
20 16 19 syl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` ( -us ` A ) ) = A )
21 20 breq2d 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) <_s ( -us ` ( -us ` A ) ) <-> ( -us ` B ) <_s A ) )
22 18 21 bitr2d 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( -us ` B ) <_s A <-> ( -us ` A ) <_s B ) )
23 14 22 mpbid 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( -us ` A ) <_s B )