Metamath Proof Explorer

Theorem addsbday

Description: The birthday of the sum of two surreals is less than or equal to the natural ordinal sum of their individual birthdays. Theorem 6.1 of Gonshor p. 95. (Contributed by Scott Fenton, 12-Aug-2025)

Ref Expression
Assertion addsbday 
|- ( ( A e. No /\ B e. No ) -> ( bday ` ( A +s B ) ) C_ ( ( bday ` A ) +no ( bday ` B ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 
 |-  ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) )
2 fveq2 
 |-  ( x = xO -> ( bday ` x ) = ( bday ` xO ) )
3 2 oveq1d 
 |-  ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) )
4 1 3 sseq12d 
 |-  ( x = xO -> ( ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) )
5 oveq2 
 |-  ( y = yO -> ( xO +s y ) = ( xO +s yO ) )
6 5 fveq2d 
 |-  ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) )
7 fveq2 
 |-  ( y = yO -> ( bday ` y ) = ( bday ` yO ) )
8 7 oveq2d 
 |-  ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) )
9 6 8 sseq12d 
 |-  ( y = yO -> ( ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) )
10 fvoveq1 
 |-  ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) )
11 2 oveq1d 
 |-  ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) )
12 10 11 sseq12d 
 |-  ( x = xO -> ( ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) <-> ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) ) )
13 fvoveq1 
 |-  ( x = A -> ( bday ` ( x +s y ) ) = ( bday ` ( A +s y ) ) )
14 fveq2 
 |-  ( x = A -> ( bday ` x ) = ( bday ` A ) )
15 14 oveq1d 
 |-  ( x = A -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` y ) ) )
16 13 15 sseq12d 
 |-  ( x = A -> ( ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) <-> ( bday ` ( A +s y ) ) C_ ( ( bday ` A ) +no ( bday ` y ) ) ) )
17 oveq2 
 |-  ( y = B -> ( A +s y ) = ( A +s B ) )
18 17 fveq2d 
 |-  ( y = B -> ( bday ` ( A +s y ) ) = ( bday ` ( A +s B ) ) )
19 fveq2 
 |-  ( y = B -> ( bday ` y ) = ( bday ` B ) )
20 19 oveq2d 
 |-  ( y = B -> ( ( bday ` A ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )
21 18 20 sseq12d 
 |-  ( y = B -> ( ( bday ` ( A +s y ) ) C_ ( ( bday ` A ) +no ( bday ` y ) ) <-> ( bday ` ( A +s B ) ) C_ ( ( bday ` A ) +no ( bday ` B ) ) ) )
22 addsval2 
 |-  ( ( x e. No /\ y e. No ) -> ( x +s y ) = ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) )
23 22 fveq2d 
 |-  ( ( x e. No /\ y e. No ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) )
24 23 adantr 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) = ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) )
25 simpl 
 |-  ( ( x e. No /\ y e. No ) -> x e. No )
26 simpr 
 |-  ( ( x e. No /\ y e. No ) -> y e. No )
27 25 26 addscut2 
 |-  ( ( x e. No /\ y e. No ) -> ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) <
28 imaundi 
 |-  ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) )
29 imaundi 
 |-  ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) )
30 imaundi 
 |-  ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) = ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) )
31 29 30 uneq12i 
 |-  ( ( bday " ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( bday " ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) )
32 28 31 eqtri 
 |-  ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) = ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) )
33 simplr 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> y e. No )
34 simpr2 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) )
35 simplr 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> y e. No )
36 leftssno 
 |-  ( _Left ` x ) C_ No
37 rightssno 
 |-  ( _Right ` x ) C_ No
38 36 37 unssi 
 |-  ( ( _Left ` x ) u. ( _Right ` x ) ) C_ No
39 38 sseli 
 |-  ( xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) -> xO e. No )
40 39 adantl 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> xO e. No )
41 35 40 addscomd 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( y +s xO ) = ( xO +s y ) )
42 41 fveq2d 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( bday ` ( y +s xO ) ) = ( bday ` ( xO +s y ) ) )
43 bdayelon 
 |-  ( bday ` y ) e. On
44 bdayelon 
 |-  ( bday ` xO ) e. On
45 naddcom 
 |-  ( ( ( bday ` y ) e. On /\ ( bday ` xO ) e. On ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) )
46 43 44 45 mp2an 
 |-  ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) )
47 46 a1i 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` y ) +no ( bday ` xO ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) )
48 42 47 sseq12d 
 |-  ( ( ( x e. No /\ y e. No ) /\ xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) -> ( ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) )
49 48 ralbidva 
 |-  ( ( x e. No /\ y e. No ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) )
50 49 adantr 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) <-> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) ) )
51 34 50 mpbird 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( y +s xO ) ) C_ ( ( bday ` y ) +no ( bday ` xO ) ) )
52 ssun1 
 |-  ( _Left ` x ) C_ ( ( _Left ` x ) u. ( _Right ` x ) )
53 33 51 52 addsbdaylem 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) )
54 36 sseli 
 |-  ( xL e. ( _Left ` x ) -> xL e. No )
55 54 adantl 
 |-  ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> xL e. No )
56 simplr 
 |-  ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> y e. No )
57 55 56 addscomd 
 |-  ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( xL +s y ) = ( y +s xL ) )
58 57 eqeq2d 
 |-  ( ( ( x e. No /\ y e. No ) /\ xL e. ( _Left ` x ) ) -> ( z = ( xL +s y ) <-> z = ( y +s xL ) ) )
59 58 rexbidva 
 |-  ( ( x e. No /\ y e. No ) -> ( E. xL e. ( _Left ` x ) z = ( xL +s y ) <-> E. xL e. ( _Left ` x ) z = ( y +s xL ) ) )
60 59 abbidv 
 |-  ( ( x e. No /\ y e. No ) -> { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } = { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } )
61 60 imaeq2d 
 |-  ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) )
62 61 adantr 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) = ( bday " { z | E. xL e. ( _Left ` x ) z = ( y +s xL ) } ) )
63 bdayelon 
 |-  ( bday ` x ) e. On
64 naddcom 
 |-  ( ( ( bday ` x ) e. On /\ ( bday ` y ) e. On ) -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` y ) +no ( bday ` x ) ) )
65 63 43 64 mp2an 
 |-  ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` y ) +no ( bday ` x ) )
66 65 a1i 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` y ) +no ( bday ` x ) ) )
67 53 62 66 3sstr4d 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
68 simpll 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> x e. No )
69 simpr3 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) )
70 ssun1 
 |-  ( _Left ` y ) C_ ( ( _Left ` y ) u. ( _Right ` y ) )
71 68 69 70 addsbdaylem 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
72 67 71 unssd 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
73 ssun2 
 |-  ( _Right ` x ) C_ ( ( _Left ` x ) u. ( _Right ` x ) )
74 33 51 73 addsbdaylem 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) C_ ( ( bday ` y ) +no ( bday ` x ) ) )
75 37 sseli 
 |-  ( xR e. ( _Right ` x ) -> xR e. No )
76 75 adantl 
 |-  ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> xR e. No )
77 simplr 
 |-  ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> y e. No )
78 76 77 addscomd 
 |-  ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( xR +s y ) = ( y +s xR ) )
79 78 eqeq2d 
 |-  ( ( ( x e. No /\ y e. No ) /\ xR e. ( _Right ` x ) ) -> ( z = ( xR +s y ) <-> z = ( y +s xR ) ) )
80 79 rexbidva 
 |-  ( ( x e. No /\ y e. No ) -> ( E. xR e. ( _Right ` x ) z = ( xR +s y ) <-> E. xR e. ( _Right ` x ) z = ( y +s xR ) ) )
81 80 abbidv 
 |-  ( ( x e. No /\ y e. No ) -> { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } = { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } )
82 81 imaeq2d 
 |-  ( ( x e. No /\ y e. No ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) )
83 82 adantr 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) = ( bday " { z | E. xR e. ( _Right ` x ) z = ( y +s xR ) } ) )
84 74 83 66 3sstr4d 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
85 ssun2 
 |-  ( _Right ` y ) C_ ( ( _Left ` y ) u. ( _Right ` y ) )
86 68 69 85 addsbdaylem 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
87 84 86 unssd 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
88 72 87 unssd 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( ( ( bday " { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } ) u. ( bday " { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) ) u. ( ( bday " { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } ) u. ( bday " { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
89 32 88 eqsstrid 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday " ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) u. ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
90 naddcl 
 |-  ( ( ( bday ` x ) e. On /\ ( bday ` y ) e. On ) -> ( ( bday ` x ) +no ( bday ` y ) ) e. On )
91 63 43 90 mp2an 
 |-  ( ( bday ` x ) +no ( bday ` y ) ) e. On
92 scutbdaybnd 
 |-  ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
93 91 92 mp3an2 
 |-  ( ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) < ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
94 27 89 93 syl2an2r 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( ( { z | E. xL e. ( _Left ` x ) z = ( xL +s y ) } u. { z | E. yL e. ( _Left ` y ) z = ( x +s yL ) } ) |s ( { z | E. xR e. ( _Right ` x ) z = ( xR +s y ) } u. { z | E. yL e. ( _Right ` y ) z = ( x +s yL ) } ) ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
95 24 94 eqsstrd 
 |-  ( ( ( x e. No /\ y e. No ) /\ ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) )
96 95 ex 
 |-  ( ( x e. No /\ y e. No ) -> ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( xO +s yO ) ) C_ ( ( bday ` xO ) +no ( bday ` yO ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( bday ` ( xO +s y ) ) C_ ( ( bday ` xO ) +no ( bday ` y ) ) /\ A. yO e. ( ( _Left ` y ) u. ( _Right ` y ) ) ( bday ` ( x +s yO ) ) C_ ( ( bday ` x ) +no ( bday ` yO ) ) ) -> ( bday ` ( x +s y ) ) C_ ( ( bday ` x ) +no ( bday ` y ) ) ) )
97 4 9 12 16 21 96 no2inds 
 |-  ( ( A e. No /\ B e. No ) -> ( bday ` ( A +s B ) ) C_ ( ( bday ` A ) +no ( bday ` B ) ) )