Metamath Proof Explorer

Theorem negsbdaylem

Description: Lemma for negsbday . Bound the birthday of the negative of a surreal number above. (Contributed by Scott Fenton, 8-Mar-2025)

Ref Expression
Assertion negsbdaylem 
|- ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) )

Proof

Step Hyp Ref Expression
1 2fveq3 
 |-  ( x = xO -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` xO ) ) )
2 fveq2 
 |-  ( x = xO -> ( bday ` x ) = ( bday ` xO ) )
3 1 2 sseq12d 
 |-  ( x = xO -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) )
4 2fveq3 
 |-  ( x = A -> ( bday ` ( -us ` x ) ) = ( bday ` ( -us ` A ) ) )
5 fveq2 
 |-  ( x = A -> ( bday ` x ) = ( bday ` A ) )
6 4 5 sseq12d 
 |-  ( x = A -> ( ( bday ` ( -us ` x ) ) C_ ( bday ` x ) <-> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) ) )
7 negsval 
 |-  ( x e. No -> ( -us ` x ) = ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) )
8 7 fveq2d 
 |-  ( x e. No -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) )
9 8 adantr 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) = ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) )
10 negscut2 
 |-  ( x e. No -> ( -us " ( _Right ` x ) ) <
11 lrold 
 |-  ( ( _Left ` x ) u. ( _Right ` x ) ) = ( _Old ` ( bday ` x ) )
12 uncom 
 |-  ( ( _Left ` x ) u. ( _Right ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) )
13 11 12 eqtr3i 
 |-  ( _Old ` ( bday ` x ) ) = ( ( _Right ` x ) u. ( _Left ` x ) )
14 13 imaeq2i 
 |-  ( -us " ( _Old ` ( bday ` x ) ) ) = ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) )
15 imaundi 
 |-  ( -us " ( ( _Right ` x ) u. ( _Left ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) )
16 14 15 eqtri 
 |-  ( -us " ( _Old ` ( bday ` x ) ) ) = ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) )
17 16 imaeq2i 
 |-  ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) = ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) )
18 11 raleqi 
 |-  ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) )
19 oldbdayim 
 |-  ( xO e. ( _Old ` ( bday ` x ) ) -> ( bday ` xO ) e. ( bday ` x ) )
20 19 adantl 
 |-  ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( bday ` xO ) e. ( bday ` x ) )
21 bdayelon 
 |-  ( bday ` ( -us ` xO ) ) e. On
22 bdayelon 
 |-  ( bday ` x ) e. On
23 ontr2 
 |-  ( ( ( bday ` ( -us ` xO ) ) e. On /\ ( bday ` x ) e. On ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
24 21 22 23 mp2an 
 |-  ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) )
25 24 a1i 
 |-  ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) /\ ( bday ` xO ) e. ( bday ` x ) ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
26 20 25 mpan2d 
 |-  ( ( x e. No /\ xO e. ( _Old ` ( bday ` x ) ) ) -> ( ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
27 26 ralimdva 
 |-  ( x e. No -> ( A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
28 27 imp 
 |-  ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) )
29 bdayfun 
 |-  Fun bday
30 imassrn 
 |-  ( -us " ( _Old ` ( bday ` x ) ) ) C_ ran -us
31 bdaydm 
 |-  dom bday = No
32 negsfo 
 |-  -us : No -onto-> No
33 forn 
 |-  ( -us : No -onto-> No -> ran -us = No )
34 32 33 ax-mp 
 |-  ran -us = No
35 31 34 eqtr4i 
 |-  dom bday = ran -us
36 30 35 sseqtrri 
 |-  ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday
37 funimass4 
 |-  ( ( Fun bday /\ ( -us " ( _Old ` ( bday ` x ) ) ) C_ dom bday ) -> ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) ) )
38 29 36 37 mp2an 
 |-  ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) )
39 negsfn 
 |-  -us Fn No
40 oldssno 
 |-  ( _Old ` ( bday ` x ) ) C_ No
41 fveq2 
 |-  ( y = ( -us ` xO ) -> ( bday ` y ) = ( bday ` ( -us ` xO ) ) )
42 41 eleq1d 
 |-  ( y = ( -us ` xO ) -> ( ( bday ` y ) e. ( bday ` x ) <-> ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
43 42 imaeqsalv 
 |-  ( ( -us Fn No /\ ( _Old ` ( bday ` x ) ) C_ No ) -> ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) ) )
44 39 40 43 mp2an 
 |-  ( A. y e. ( -us " ( _Old ` ( bday ` x ) ) ) ( bday ` y ) e. ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) )
45 38 44 bitri 
 |-  ( ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) <-> A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) e. ( bday ` x ) )
46 28 45 sylibr 
 |-  ( ( x e. No /\ A. xO e. ( _Old ` ( bday ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) )
47 18 46 sylan2b 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( -us " ( _Old ` ( bday ` x ) ) ) ) C_ ( bday ` x ) )
48 17 47 eqsstrrid 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday " ( ( -us " ( _Right ` x ) ) u. ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) )
49 scutbdaybnd 
 |-  ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) )
50 22 49 mp3an2 
 |-  ( ( ( -us " ( _Right ` x ) ) < ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) )
51 10 48 50 syl2an2r 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( ( -us " ( _Right ` x ) ) |s ( -us " ( _Left ` x ) ) ) ) C_ ( bday ` x ) )
52 9 51 eqsstrd 
 |-  ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) )
53 52 ex 
 |-  ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( -us ` xO ) ) C_ ( bday ` xO ) -> ( bday ` ( -us ` x ) ) C_ ( bday ` x ) ) )
54 3 6 53 noinds 
 |-  ( A e. No -> ( bday ` ( -us ` A ) ) C_ ( bday ` A ) )