Metamath Proof Explorer

Theorem onsbnd

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

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

Proof

Step Hyp Ref Expression
1 ral0 
 |-  A. xR e. (/) B
2 1 a1i 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A. xR e. (/) B
3 leftssold 
 |-  ( _Left ` B ) C_ ( _Old ` ( bday ` B ) )
4 bdayelon 
 |-  ( bday ` A ) e. On
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 oldss 
 |-  ( ( ( bday ` A ) e. On /\ ( bday ` B ) C_ ( bday ` A ) ) -> ( _Old ` ( bday ` B ) ) C_ ( _Old ` ( bday ` A ) ) )
8 4 6 7 sylancr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Old ` ( bday ` B ) ) C_ ( _Old ` ( bday ` A ) ) )
9 3 8 sstrid 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Left ` B ) C_ ( _Old ` ( bday ` A ) ) )
10 onsleft 
 |-  ( A e. On_s -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
11 10 adantr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Old ` ( bday ` A ) ) = ( _Left ` A ) )
12 9 11 sseqtrd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Left ` B ) C_ ( _Left ` A ) )
13 12 sselda 
 |-  ( ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) /\ yL e. ( _Left ` B ) ) -> yL e. ( _Left ` A ) )
14 leftlt 
 |-  ( yL e. ( _Left ` A ) -> yL
15 13 14 syl 
 |-  ( ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) /\ yL e. ( _Left ` B ) ) -> yL
16 15 ralrimiva 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A. yL e. ( _Left ` B ) yL
17 lltropt 
 |-  ( _Left ` B ) <
18 17 a1i 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Left ` B ) <
19 leftssno 
 |-  ( _Left ` A ) C_ No
20 fvex 
 |-  ( _Left ` A ) e. _V
21 20 elpw 
 |-  ( ( _Left ` A ) e. ~P No <-> ( _Left ` A ) C_ No )
22 19 21 mpbir 
 |-  ( _Left ` A ) e. ~P No
23 nulssgt 
 |-  ( ( _Left ` A ) e. ~P No -> ( _Left ` A ) <
24 22 23 mp1i 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( _Left ` A ) <
25 madessno 
 |-  ( _Made ` ( bday ` A ) ) C_ No
26 25 sseli 
 |-  ( B e. ( _Made ` ( bday ` A ) ) -> B e. No )
27 26 adantl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> B e. No )
28 lrcut 
 |-  ( B e. No -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
29 27 28 syl 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( ( _Left ` B ) |s ( _Right ` B ) ) = B )
30 29 eqcomd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> B = ( ( _Left ` B ) |s ( _Right ` B ) ) )
31 onscutleft 
 |-  ( A e. On_s -> A = ( ( _Left ` A ) |s (/) ) )
32 31 adantr 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> A = ( ( _Left ` A ) |s (/) ) )
33 18 24 30 32 slerecd 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> ( B <_s A <-> ( A. xR e. (/) B
34 2 16 33 mpbir2and 
 |-  ( ( A e. On_s /\ B e. ( _Made ` ( bday ` A ) ) ) -> B <_s A )