Metamath Proof Explorer

Theorem addsonbday

Description: The birthday of the sum of two ordinals is the natural sum of their birthdays. (Contributed by Scott Fenton, 22-Feb-2026)

Ref Expression
Assertion addsonbday 
|- ( ( A e. On_s /\ B e. On_s ) -> ( bday ` ( A +s B ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )

Proof

Step Hyp Ref Expression
1 onsno 
 |-  ( A e. On_s -> A e. No )
2 onsno 
 |-  ( B e. On_s -> B e. No )
3 addsbday 
 |-  ( ( A e. No /\ B e. No ) -> ( bday ` ( A +s B ) ) C_ ( ( bday ` A ) +no ( bday ` B ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( bday ` ( A +s B ) ) C_ ( ( bday ` A ) +no ( bday ` B ) ) )
5 fveq2 
 |-  ( x = xO -> ( bday ` x ) = ( bday ` xO ) )
6 5 oveq1d 
 |-  ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) )
7 fvoveq1 
 |-  ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) )
8 6 7 sseq12d 
 |-  ( x = xO -> ( ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) )
9 fveq2 
 |-  ( y = yO -> ( bday ` y ) = ( bday ` yO ) )
10 9 oveq2d 
 |-  ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) )
11 oveq2 
 |-  ( y = yO -> ( xO +s y ) = ( xO +s yO ) )
12 11 fveq2d 
 |-  ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) )
13 10 12 sseq12d 
 |-  ( y = yO -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) )
14 5 oveq1d 
 |-  ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) )
15 fvoveq1 
 |-  ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) )
16 14 15 sseq12d 
 |-  ( x = xO -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) )
17 fveq2 
 |-  ( x = A -> ( bday ` x ) = ( bday ` A ) )
18 17 oveq1d 
 |-  ( x = A -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` y ) ) )
19 fvoveq1 
 |-  ( x = A -> ( bday ` ( x +s y ) ) = ( bday ` ( A +s y ) ) )
20 18 19 sseq12d 
 |-  ( x = A -> ( ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) <-> ( ( bday ` A ) +no ( bday ` y ) ) C_ ( bday ` ( A +s y ) ) ) )
21 fveq2 
 |-  ( y = B -> ( bday ` y ) = ( bday ` B ) )
22 21 oveq2d 
 |-  ( y = B -> ( ( bday ` A ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )
23 oveq2 
 |-  ( y = B -> ( A +s y ) = ( A +s B ) )
24 23 fveq2d 
 |-  ( y = B -> ( bday ` ( A +s y ) ) = ( bday ` ( A +s B ) ) )
25 22 24 sseq12d 
 |-  ( y = B -> ( ( ( bday ` A ) +no ( bday ` y ) ) C_ ( bday ` ( A +s y ) ) <-> ( ( bday ` A ) +no ( bday ` B ) ) C_ ( bday ` ( A +s B ) ) ) )
26 bdayelon 
 |-  ( bday ` x ) e. On
27 bdayelon 
 |-  ( bday ` y ) e. On
28 naddov2 
 |-  ( ( ( bday ` x ) e. On /\ ( bday ` y ) e. On ) -> ( ( bday ` x ) +no ( bday ` y ) ) = |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } )
29 26 27 28 mp2an 
 |-  ( ( bday ` x ) +no ( bday ` y ) ) = |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) }
30 27 oneli 
 |-  ( q e. ( bday ` y ) -> q e. On )
31 breq1 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( yO  ( `' ( bday |` On_s ) ` q )
32 fveq2 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` yO ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) )
33 32 oveq2d 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) )
34 oveq2 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( x +s yO ) = ( x +s ( `' ( bday |` On_s ) ` q ) ) )
35 34 fveq2d 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` ( x +s yO ) ) = ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) )
36 33 35 sseq12d 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) )
37 31 36 imbi12d 
 |-  ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) <-> ( ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) )
38 simplr3 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) )
39 onsiso 
 |-  ( bday |` On_s ) Isom
40 isof1o 
 |-  ( ( bday |` On_s ) Isom  ( bday |` On_s ) : On_s -1-1-onto-> On )
41 39 40 ax-mp 
 |-  ( bday |` On_s ) : On_s -1-1-onto-> On
42 f1ocnvdm 
 |-  ( ( ( bday |` On_s ) : On_s -1-1-onto-> On /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. On_s )
43 41 42 mpan 
 |-  ( q e. On -> ( `' ( bday |` On_s ) ` q ) e. On_s )
44 43 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. On_s )
45 37 38 44 rspcdva 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) )
46 45 impr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) )
47 onsno 
 |-  ( ( `' ( bday |` On_s ) ` q ) e. On_s -> ( `' ( bday |` On_s ) ` q ) e. No )
48 44 47 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. No )
49 simpllr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. On_s )
50 onsno 
 |-  ( y e. On_s -> y e. No )
51 49 50 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. No )
52 simplll 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. On_s )
53 onsno 
 |-  ( x e. On_s -> x e. No )
54 52 53 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. No )
55 48 51 54 sltadd2d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( x +s ( `' ( bday |` On_s ) ` q ) )
56 onaddscl 
 |-  ( ( x e. On_s /\ ( `' ( bday |` On_s ) ` q ) e. On_s ) -> ( x +s ( `' ( bday |` On_s ) ` q ) ) e. On_s )
57 52 44 56 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s ( `' ( bday |` On_s ) ` q ) ) e. On_s )
58 onaddscl 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( x +s y ) e. On_s )
59 58 ad2antrr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s y ) e. On_s )
60 onslt 
 |-  ( ( ( x +s ( `' ( bday |` On_s ) ` q ) ) e. On_s /\ ( x +s y ) e. On_s ) -> ( ( x +s ( `' ( bday |` On_s ) ` q ) )  ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
61 57 59 60 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( x +s ( `' ( bday |` On_s ) ` q ) )  ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
62 55 61 bitrd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
63 62 biimpd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
64 63 impr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q )  ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) )
65 bdayelon 
 |-  ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. On
66 naddcl 
 |-  ( ( ( bday ` x ) e. On /\ ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. On ) -> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. On )
67 26 65 66 mp2an 
 |-  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. On
68 67 onordi 
 |-  Ord ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) )
69 bdayelon 
 |-  ( bday ` ( x +s y ) ) e. On
70 69 onordi 
 |-  Ord ( bday ` ( x +s y ) )
71 ordtr2 
 |-  ( ( Ord ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) /\ Ord ( bday ` ( x +s y ) ) ) -> ( ( ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) /\ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) -> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
72 68 70 71 mp2an 
 |-  ( ( ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) /\ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) -> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) )
73 46 64 72 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) )
74 73 expr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
75 43 fvresd 
 |-  ( q e. On -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) )
76 75 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) )
77 76 oveq2d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) )
78 77 eleq1d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
79 74 78 sylibrd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) )
80 onslt 
 |-  ( ( ( `' ( bday |` On_s ) ` q ) e. On_s /\ y e. On_s ) -> ( ( `' ( bday |` On_s ) ` q )  ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) ) )
81 44 49 80 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) ) )
82 f1ocnvfv2 
 |-  ( ( ( bday |` On_s ) : On_s -1-1-onto-> On /\ q e. On ) -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = q )
83 41 82 mpan 
 |-  ( q e. On -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = q )
84 75 83 eqtr3d 
 |-  ( q e. On -> ( bday ` ( `' ( bday |` On_s ) ` q ) ) = q )
85 84 eleq1d 
 |-  ( q e. On -> ( ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) <-> q e. ( bday ` y ) ) )
86 85 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) <-> q e. ( bday ` y ) ) )
87 81 86 bitrd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q )  q e. ( bday ` y ) ) )
88 83 oveq2d 
 |-  ( q e. On -> ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) = ( ( bday ` x ) +no q ) )
89 88 eleq1d 
 |-  ( q e. On -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
90 89 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
91 79 87 90 3imtr3d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
92 91 ex 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. On -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) )
93 30 92 syl5 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) )
94 93 pm2.43d 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
95 94 ralrimiv 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) )
96 26 oneli 
 |-  ( p e. ( bday ` x ) -> p e. On )
97 breq1 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( xO  ( `' ( bday |` On_s ) ` p )
98 fveq2 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` xO ) = ( bday ` ( `' ( bday |` On_s ) ` p ) ) )
99 98 oveq1d 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) )
100 fvoveq1 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` ( xO +s y ) ) = ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) )
101 99 100 sseq12d 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) )
102 97 101 imbi12d 
 |-  ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) <-> ( ( `' ( bday |` On_s ) ` p )  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) )
103 simplr2 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) )
104 f1ocnvdm 
 |-  ( ( ( bday |` On_s ) : On_s -1-1-onto-> On /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. On_s )
105 41 104 mpan 
 |-  ( p e. On -> ( `' ( bday |` On_s ) ` p ) e. On_s )
106 105 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. On_s )
107 102 103 106 rspcdva 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) )
108 107 impr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p )  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) )
109 onsno 
 |-  ( ( `' ( bday |` On_s ) ` p ) e. On_s -> ( `' ( bday |` On_s ) ` p ) e. No )
110 106 109 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. No )
111 simplll 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. On_s )
112 111 53 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. No )
113 simpllr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. On_s )
114 113 50 syl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. No )
115 110 112 114 sltadd1d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( ( `' ( bday |` On_s ) ` p ) +s y )
116 onaddscl 
 |-  ( ( ( `' ( bday |` On_s ) ` p ) e. On_s /\ y e. On_s ) -> ( ( `' ( bday |` On_s ) ` p ) +s y ) e. On_s )
117 106 113 116 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) +s y ) e. On_s )
118 58 ad2antrr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( x +s y ) e. On_s )
119 onslt 
 |-  ( ( ( ( `' ( bday |` On_s ) ` p ) +s y ) e. On_s /\ ( x +s y ) e. On_s ) -> ( ( ( `' ( bday |` On_s ) ` p ) +s y )  ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) )
120 117 118 119 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( `' ( bday |` On_s ) ` p ) +s y )  ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) )
121 115 120 bitrd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) )
122 121 biimpd 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) )
123 122 impr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p )  ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) )
124 bdayelon 
 |-  ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. On
125 naddcl 
 |-  ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. On /\ ( bday ` y ) e. On ) -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. On )
126 124 27 125 mp2an 
 |-  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. On
127 126 onordi 
 |-  Ord ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) )
128 ordtr2 
 |-  ( ( Ord ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) /\ Ord ( bday ` ( x +s y ) ) ) -> ( ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) /\ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
129 127 70 128 mp2an 
 |-  ( ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) /\ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) )
130 108 123 129 syl2anc 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p )  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) )
131 130 expr 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
132 onslt 
 |-  ( ( ( `' ( bday |` On_s ) ` p ) e. On_s /\ x e. On_s ) -> ( ( `' ( bday |` On_s ) ` p )  ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. ( bday ` x ) ) )
133 105 132 sylan 
 |-  ( ( p e. On /\ x e. On_s ) -> ( ( `' ( bday |` On_s ) ` p )  ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. ( bday ` x ) ) )
134 133 ancoms 
 |-  ( ( x e. On_s /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. ( bday ` x ) ) )
135 105 fvresd 
 |-  ( p e. On -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` p ) ) = ( bday ` ( `' ( bday |` On_s ) ` p ) ) )
136 f1ocnvfv2 
 |-  ( ( ( bday |` On_s ) : On_s -1-1-onto-> On /\ p e. On ) -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` p ) ) = p )
137 41 136 mpan 
 |-  ( p e. On -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` p ) ) = p )
138 135 137 eqtr3d 
 |-  ( p e. On -> ( bday ` ( `' ( bday |` On_s ) ` p ) ) = p )
139 138 eleq1d 
 |-  ( p e. On -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. ( bday ` x ) <-> p e. ( bday ` x ) ) )
140 139 adantl 
 |-  ( ( x e. On_s /\ p e. On ) -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) e. ( bday ` x ) <-> p e. ( bday ` x ) ) )
141 134 140 bitrd 
 |-  ( ( x e. On_s /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  p e. ( bday ` x ) ) )
142 141 ad4ant14 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p )  p e. ( bday ` x ) ) )
143 138 oveq1d 
 |-  ( p e. On -> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) = ( p +no ( bday ` y ) ) )
144 143 eleq1d 
 |-  ( p e. On -> ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) <-> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
145 144 adantl 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) <-> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
146 131 142 145 3imtr3d 
 |-  ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
147 146 ex 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. On -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) )
148 96 147 syl5 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) )
149 148 pm2.43d 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
150 149 ralrimiv 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) )
151 eleq2 
 |-  ( a = ( bday ` ( x +s y ) ) -> ( ( ( bday ` x ) +no q ) e. a <-> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
152 151 ralbidv 
 |-  ( a = ( bday ` ( x +s y ) ) -> ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a <-> A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) )
153 eleq2 
 |-  ( a = ( bday ` ( x +s y ) ) -> ( ( p +no ( bday ` y ) ) e. a <-> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
154 153 ralbidv 
 |-  ( a = ( bday ` ( x +s y ) ) -> ( A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a <-> A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
155 152 154 anbi12d 
 |-  ( a = ( bday ` ( x +s y ) ) -> ( ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) <-> ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) )
156 155 elrab3 
 |-  ( ( bday ` ( x +s y ) ) e. On -> ( ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } <-> ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) )
157 69 156 ax-mp 
 |-  ( ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } <-> ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) )
158 95 150 157 sylanbrc 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } )
159 intss1 
 |-  ( ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } -> |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } C_ ( bday ` ( x +s y ) ) )
160 158 159 syl 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } C_ ( bday ` ( x +s y ) ) )
161 29 160 eqsstrid 
 |-  ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) )
162 161 ex 
 |-  ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO  ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO  ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO  ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) ) )
163 8 13 16 20 25 162 ons2ind 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( ( bday ` A ) +no ( bday ` B ) ) C_ ( bday ` ( A +s B ) ) )
164 4 163 eqssd 
 |-  ( ( A e. On_s /\ B e. On_s ) -> ( bday ` ( A +s B ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )