Metamath Proof Explorer

Theorem addsprop

Description: Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of Gonshor p. 14. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Assertion addsprop 
|- ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )

Proof

Step Hyp Ref Expression
1 bdayelon 
 |-  ( bday ` X ) e. On
2 bdayelon 
 |-  ( bday ` Y ) e. On
3 naddcl 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` Y ) e. On ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. On )
4 1 2 3 mp2an 
 |-  ( ( bday ` X ) +no ( bday ` Y ) ) e. On
5 bdayelon 
 |-  ( bday ` Z ) e. On
6 naddcl 
 |-  ( ( ( bday ` X ) e. On /\ ( bday ` Z ) e. On ) -> ( ( bday ` X ) +no ( bday ` Z ) ) e. On )
7 1 5 6 mp2an 
 |-  ( ( bday ` X ) +no ( bday ` Z ) ) e. On
8 4 7 onun2i 
 |-  ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On
9 risset 
 |-  ( ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) e. On <-> E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
10 8 9 mpbi 
 |-  E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) )
11 eqeq1 
 |-  ( a = b -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) )
12 11 imbi1d 
 |-  ( a = b -> ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
13 12 ralbidv 
 |-  ( a = b -> ( A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
14 13 2ralbidv 
 |-  ( a = b -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. x e. No A. y e. No A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
15 fveq2 
 |-  ( x = p -> ( bday ` x ) = ( bday ` p ) )
16 15 oveq1d 
 |-  ( x = p -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` y ) ) )
17 15 oveq1d 
 |-  ( x = p -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` z ) ) )
18 16 17 uneq12d 
 |-  ( x = p -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) )
19 18 eqeq2d 
 |-  ( x = p -> ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) )
20 oveq1 
 |-  ( x = p -> ( x +s y ) = ( p +s y ) )
21 20 eleq1d 
 |-  ( x = p -> ( ( x +s y ) e. No <-> ( p +s y ) e. No ) )
22 oveq2 
 |-  ( x = p -> ( y +s x ) = ( y +s p ) )
23 oveq2 
 |-  ( x = p -> ( z +s x ) = ( z +s p ) )
24 22 23 breq12d 
 |-  ( x = p -> ( ( y +s x )  ( y +s p )
25 24 imbi2d 
 |-  ( x = p -> ( ( y  ( y +s x )  ( y  ( y +s p )
26 21 25 anbi12d 
 |-  ( x = p -> ( ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( ( p +s y ) e. No /\ ( y  ( y +s p )
27 19 26 imbi12d 
 |-  ( x = p -> ( ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y  ( y +s p )
28 fveq2 
 |-  ( y = q -> ( bday ` y ) = ( bday ` q ) )
29 28 oveq2d 
 |-  ( y = q -> ( ( bday ` p ) +no ( bday ` y ) ) = ( ( bday ` p ) +no ( bday ` q ) ) )
30 29 uneq1d 
 |-  ( y = q -> ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) )
31 30 eqeq2d 
 |-  ( y = q -> ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) ) )
32 oveq2 
 |-  ( y = q -> ( p +s y ) = ( p +s q ) )
33 32 eleq1d 
 |-  ( y = q -> ( ( p +s y ) e. No <-> ( p +s q ) e. No ) )
34 breq1 
 |-  ( y = q -> ( y  q
35 oveq1 
 |-  ( y = q -> ( y +s p ) = ( q +s p ) )
36 35 breq1d 
 |-  ( y = q -> ( ( y +s p )  ( q +s p )
37 34 36 imbi12d 
 |-  ( y = q -> ( ( y  ( y +s p )  ( q  ( q +s p )
38 33 37 anbi12d 
 |-  ( y = q -> ( ( ( p +s y ) e. No /\ ( y  ( y +s p )  ( ( p +s q ) e. No /\ ( q  ( q +s p )
39 31 38 imbi12d 
 |-  ( y = q -> ( ( b = ( ( ( bday ` p ) +no ( bday ` y ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s y ) e. No /\ ( y  ( y +s p )  ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
40 fveq2 
 |-  ( z = r -> ( bday ` z ) = ( bday ` r ) )
41 40 oveq2d 
 |-  ( z = r -> ( ( bday ` p ) +no ( bday ` z ) ) = ( ( bday ` p ) +no ( bday ` r ) ) )
42 41 uneq2d 
 |-  ( z = r -> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) )
43 42 eqeq2d 
 |-  ( z = r -> ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) <-> b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) ) )
44 breq2 
 |-  ( z = r -> ( q  q
45 oveq1 
 |-  ( z = r -> ( z +s p ) = ( r +s p ) )
46 45 breq2d 
 |-  ( z = r -> ( ( q +s p )  ( q +s p )
47 44 46 imbi12d 
 |-  ( z = r -> ( ( q  ( q +s p )  ( q  ( q +s p )
48 47 anbi2d 
 |-  ( z = r -> ( ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( ( p +s q ) e. No /\ ( q  ( q +s p )
49 43 48 imbi12d 
 |-  ( z = r -> ( ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
50 27 39 49 cbvral3vw 
 |-  ( A. x e. No A. y e. No A. z e. No ( b = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
51 14 50 bitrdi 
 |-  ( a = b -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
52 ralrot3 
 |-  ( A. p e. No A. q e. No A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
53 ralcom 
 |-  ( A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. r e. No A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
54 r19.23v 
 |-  ( A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
55 risset 
 |-  ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) )
56 55 imbi1i 
 |-  ( ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( E. b e. a b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
57 54 56 bitr4i 
 |-  ( A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
58 57 ralbii 
 |-  ( A. r e. No A. b e. a ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
59 53 58 bitri 
 |-  ( A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
60 59 2ralbii 
 |-  ( A. p e. No A. q e. No A. b e. a A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
61 52 60 bitr3i 
 |-  ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
62 eleq2 
 |-  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a <-> ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) ) )
63 62 imbi1d 
 |-  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
64 63 ralbidv 
 |-  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
65 64 2ralbidv 
 |-  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
66 65 anbi1d 
 |-  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
67 66 biimpcd 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
68 simpl 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
69 simprll 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  x e. No )
70 simprlr 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  y e. No )
71 68 69 70 addsproplem3 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( ( x +s y ) e. No /\ ( { a | E. b e. ( _Left ` x ) a = ( b +s y ) } u. { c | E. d e. ( _Left ` y ) c = ( x +s d ) } ) <
72 71 simp1d 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( x +s y ) e. No )
73 68 adantr 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )
74 69 adantr 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  x e. No )
75 70 adantr 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  y e. No )
76 simplrr 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  z e. No )
77 simpr 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  y
78 73 74 75 76 77 addsproplem7 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( y +s x )
79 78 ex 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( y  ( y +s x )
80 72 79 jca 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( ( x +s y ) e. No /\ ( y  ( y +s x )
81 67 80 syl6 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
82 81 anassrs 
 |-  ( ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
83 82 ralrimiva 
 |-  ( ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
84 83 ralrimivva 
 |-  ( A. p e. No A. q e. No A. r e. No ( ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) e. a -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
85 61 84 sylbi 
 |-  ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
86 85 a1i 
 |-  ( a e. On -> ( A. b e. a A. p e. No A. q e. No A. r e. No ( b = ( ( ( bday ` p ) +no ( bday ` q ) ) u. ( ( bday ` p ) +no ( bday ` r ) ) ) -> ( ( p +s q ) e. No /\ ( q  ( q +s p )  A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
87 51 86 tfis2 
 |-  ( a e. On -> A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )
88 fveq2 
 |-  ( x = X -> ( bday ` x ) = ( bday ` X ) )
89 88 oveq1d 
 |-  ( x = X -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` y ) ) )
90 88 oveq1d 
 |-  ( x = X -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` z ) ) )
91 89 90 uneq12d 
 |-  ( x = X -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) )
92 91 eqeq2d 
 |-  ( x = X -> ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) )
93 oveq1 
 |-  ( x = X -> ( x +s y ) = ( X +s y ) )
94 93 eleq1d 
 |-  ( x = X -> ( ( x +s y ) e. No <-> ( X +s y ) e. No ) )
95 oveq2 
 |-  ( x = X -> ( y +s x ) = ( y +s X ) )
96 oveq2 
 |-  ( x = X -> ( z +s x ) = ( z +s X ) )
97 95 96 breq12d 
 |-  ( x = X -> ( ( y +s x )  ( y +s X )
98 97 imbi2d 
 |-  ( x = X -> ( ( y  ( y +s x )  ( y  ( y +s X )
99 94 98 anbi12d 
 |-  ( x = X -> ( ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( ( X +s y ) e. No /\ ( y  ( y +s X )
100 92 99 imbi12d 
 |-  ( x = X -> ( ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y  ( y +s X )
101 fveq2 
 |-  ( y = Y -> ( bday ` y ) = ( bday ` Y ) )
102 101 oveq2d 
 |-  ( y = Y -> ( ( bday ` X ) +no ( bday ` y ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) )
103 102 uneq1d 
 |-  ( y = Y -> ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) )
104 103 eqeq2d 
 |-  ( y = Y -> ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) ) )
105 oveq2 
 |-  ( y = Y -> ( X +s y ) = ( X +s Y ) )
106 105 eleq1d 
 |-  ( y = Y -> ( ( X +s y ) e. No <-> ( X +s Y ) e. No ) )
107 breq1 
 |-  ( y = Y -> ( y  Y
108 oveq1 
 |-  ( y = Y -> ( y +s X ) = ( Y +s X ) )
109 108 breq1d 
 |-  ( y = Y -> ( ( y +s X )  ( Y +s X )
110 107 109 imbi12d 
 |-  ( y = Y -> ( ( y  ( y +s X )  ( Y  ( Y +s X )
111 106 110 anbi12d 
 |-  ( y = Y -> ( ( ( X +s y ) e. No /\ ( y  ( y +s X )  ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
112 104 111 imbi12d 
 |-  ( y = Y -> ( ( a = ( ( ( bday ` X ) +no ( bday ` y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s y ) e. No /\ ( y  ( y +s X )  ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
113 fveq2 
 |-  ( z = Z -> ( bday ` z ) = ( bday ` Z ) )
114 113 oveq2d 
 |-  ( z = Z -> ( ( bday ` X ) +no ( bday ` z ) ) = ( ( bday ` X ) +no ( bday ` Z ) ) )
115 114 uneq2d 
 |-  ( z = Z -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
116 115 eqeq2d 
 |-  ( z = Z -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) <-> a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) )
117 breq2 
 |-  ( z = Z -> ( Y  Y
118 oveq1 
 |-  ( z = Z -> ( z +s X ) = ( Z +s X ) )
119 118 breq2d 
 |-  ( z = Z -> ( ( Y +s X )  ( Y +s X )
120 117 119 imbi12d 
 |-  ( z = Z -> ( ( Y  ( Y +s X )  ( Y  ( Y +s X )
121 120 anbi2d 
 |-  ( z = Z -> ( ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )  ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
122 116 121 imbi12d 
 |-  ( z = Z -> ( ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )  ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
123 100 112 122 rspc3v 
 |-  ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( A. x e. No A. y e. No A. z e. No ( a = ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) -> ( ( x +s y ) e. No /\ ( y  ( y +s x )  ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
124 87 123 syl5com 
 |-  ( a e. On -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
125 124 com23 
 |-  ( a e. On -> ( a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
126 125 rexlimiv 
 |-  ( E. a e. On a = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )
127 10 126 ax-mp 
 |-  ( ( X e. No /\ Y e. No /\ Z e. No ) -> ( ( X +s Y ) e. No /\ ( Y  ( Y +s X )