Metamath Proof Explorer

Theorem addsproplem2

Description: Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2 , it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

Ref Expression
Hypotheses addsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
addsproplem2.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
addsproplem2.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
Assertion addsproplem2 ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )

Proof

Step Hyp Ref Expression
1 addsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
2 addsproplem2.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
3 addsproplem2.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
4 fvex ⊢ ( L ‘ 𝑋 ) ∈ V
5 4 abrexex ⊢ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V
6 5 a1i ⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V )
7 fvex ⊢ ( L ‘ 𝑌 ) ∈ V
8 7 abrexex ⊢ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V
9 8 a1i ⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V )
10 6 9 unexd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∈ V )
11 fvex ⊢ ( R ‘ 𝑋 ) ∈ V
12 11 abrexex ⊢ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V
13 12 a1i ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V )
14 fvex ⊢ ( R ‘ 𝑌 ) ∈ V
15 14 abrexex ⊢ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V
16 15 a1i ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V )
17 13 16 unexd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ∈ V )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
19 leftssno ⊢ ( L ‘ 𝑋 ) ⊆ No
20 19 sseli ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ No )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑙 ∈ No )
22 3 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑌 ∈ No )
23 0sno ⊢ 0s ∈ No
24 23 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 0s ∈ No )
25 bday0s ⊢ ( bday ‘ 0s ) = ∅
26 25 oveq2i ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑙 ) +no ∅ )
27 bdayelon ⊢ ( bday ‘ 𝑙 ) ∈ On
28 naddrid ⊢ ( ( bday ‘ 𝑙 ) ∈ On → ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 ) )
29 27 28 ax-mp ⊢ ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 )
30 26 29 eqtri ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑙 )
31 30 uneq2i ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) )
32 bdayelon ⊢ ( bday ‘ 𝑌 ) ∈ On
33 naddword1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
34 27 32 33 mp2an ⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
35 ssequn2 ⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
36 34 35 mpbi ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
37 31 36 eqtri ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
38 leftssold ⊢ ( L ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
39 38 sseli ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
40 bdayelon ⊢ ( bday ‘ 𝑋 ) ∈ On
41 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑙 ∈ No ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
42 40 20 41 sylancr ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
43 39 42 mpbid ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) )
44 naddel1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
45 27 40 32 44 mp3an ⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
46 43 45 sylib ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
48 elun1 ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
49 47 48 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
50 37 49 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
51 18 21 22 24 50 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
52 51 simpld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
53 eleq1a ⊢ ( ( 𝑙 +s 𝑌 ) ∈ No → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
54 52 53 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
55 54 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
56 55 abssdv ⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ⊆ No )
57 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
58 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑋 ∈ No )
59 leftssno ⊢ ( L ‘ 𝑌 ) ⊆ No
60 59 sseli ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ No )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑚 ∈ No )
62 23 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 0s ∈ No )
63 25 oveq2i ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑋 ) +no ∅ )
64 naddrid ⊢ ( ( bday ‘ 𝑋 ) ∈ On → ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 ) )
65 40 64 ax-mp ⊢ ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 )
66 63 65 eqtri ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑋 )
67 66 uneq2i ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) )
68 bdayelon ⊢ ( bday ‘ 𝑚 ) ∈ On
69 naddword1 ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
70 40 68 69 mp2an ⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
71 ssequn2 ⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
72 70 71 mpbi ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
73 67 72 eqtri ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
74 leftssold ⊢ ( L ‘ 𝑌 ) ⊆ ( O ‘ ( bday ‘ 𝑌 ) )
75 74 sseli ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
76 oldbday ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑚 ∈ No ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
77 32 60 76 sylancr ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
78 75 77 mpbid ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) )
79 naddel2 ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
80 68 32 40 79 mp3an ⊢ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
81 78 80 sylib ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
82 81 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
83 elun1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
84 82 83 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
85 73 84 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
86 57 58 61 62 85 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
87 86 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
88 eleq1a ⊢ ( ( 𝑋 +s 𝑚 ) ∈ No → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
89 87 88 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
90 89 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
91 90 abssdv ⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ⊆ No )
92 56 91 unssd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ⊆ No )
93 1 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
94 rightssno ⊢ ( R ‘ 𝑋 ) ⊆ No
95 94 sseli ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ No )
96 95 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑟 ∈ No )
97 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑌 ∈ No )
98 23 a1i ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 0s ∈ No )
99 25 oveq2i ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑟 ) +no ∅ )
100 bdayelon ⊢ ( bday ‘ 𝑟 ) ∈ On
101 naddrid ⊢ ( ( bday ‘ 𝑟 ) ∈ On → ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 ) )
102 100 101 ax-mp ⊢ ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 )
103 99 102 eqtri ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑟 )
104 103 uneq2i ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) )
105 naddword1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
106 100 32 105 mp2an ⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
107 ssequn2 ⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
108 106 107 mpbi ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
109 104 108 eqtri ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
110 rightssold ⊢ ( R ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
111 110 sseli ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
112 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑟 ∈ No ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
113 40 95 112 sylancr ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
114 111 113 mpbid ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) )
115 naddel1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
116 100 40 32 115 mp3an ⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
117 114 116 sylib ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
119 elun1 ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
120 118 119 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
121 109 120 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
122 93 96 97 98 121 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
123 122 simpld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
124 eleq1a ⊢ ( ( 𝑟 +s 𝑌 ) ∈ No → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
125 123 124 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
126 125 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
127 126 abssdv ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ⊆ No )
128 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
129 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑋 ∈ No )
130 rightssno ⊢ ( R ‘ 𝑌 ) ⊆ No
131 130 sseli ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ No )
132 131 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑠 ∈ No )
133 23 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 0s ∈ No )
134 66 uneq2i ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) )
135 bdayelon ⊢ ( bday ‘ 𝑠 ) ∈ On
136 naddword1 ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
137 40 135 136 mp2an ⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
138 ssequn2 ⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
139 137 138 mpbi ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
140 134 139 eqtri ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
141 rightssold ⊢ ( R ‘ 𝑌 ) ⊆ ( O ‘ ( bday ‘ 𝑌 ) )
142 141 sseli ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
143 oldbday ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑠 ∈ No ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
144 32 131 143 sylancr ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
145 142 144 mpbid ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) )
146 naddel2 ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
147 135 32 40 146 mp3an ⊢ ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
148 145 147 sylib ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
149 148 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
150 elun1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
151 149 150 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
152 140 151 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
153 128 129 132 133 152 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
154 153 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
155 eleq1a ⊢ ( ( 𝑋 +s 𝑠 ) ∈ No → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
156 154 155 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
157 156 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
158 157 abssdv ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ⊆ No )
159 127 158 unssd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ⊆ No )
160 elun ⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) )
161 vex ⊢ 𝑎 ∈ V
162 eqeq1 ⊢ ( 𝑝 = 𝑎 → ( 𝑝 = ( 𝑙 +s 𝑌 ) ↔ 𝑎 = ( 𝑙 +s 𝑌 ) ) )
163 162 rexbidv ⊢ ( 𝑝 = 𝑎 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ) )
164 161 163 elab ⊢ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) )
165 eqeq1 ⊢ ( 𝑞 = 𝑎 → ( 𝑞 = ( 𝑋 +s 𝑚 ) ↔ 𝑎 = ( 𝑋 +s 𝑚 ) ) )
166 165 rexbidv ⊢ ( 𝑞 = 𝑎 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
167 161 166 elab ⊢ ( 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) )
168 164 167 orbi12i ⊢ ( ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
169 160 168 bitri ⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
170 elun ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )
171 vex ⊢ 𝑏 ∈ V
172 eqeq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 = ( 𝑟 +s 𝑌 ) ↔ 𝑏 = ( 𝑟 +s 𝑌 ) ) )
173 172 rexbidv ⊢ ( 𝑤 = 𝑏 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
174 171 173 elab ⊢ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) )
175 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝑋 +s 𝑠 ) ↔ 𝑏 = ( 𝑋 +s 𝑠 ) ) )
176 175 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
177 171 176 elab ⊢ ( 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) )
178 174 177 orbi12i ⊢ ( ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
179 170 178 bitri ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
180 169 179 anbi12i ⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) )
181 anddi ⊢ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
182 180 181 bitri ⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
183 reeanv ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
184 lltropt ⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
185 184 a1i ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
186 simprl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ ( L ‘ 𝑋 ) )
187 simprr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ ( R ‘ 𝑋 ) )
188 185 186 187 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 <s 𝑟 )
189 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
190 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
191 20 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ No )
192 95 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
193 naddcom ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
194 32 27 193 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
195 46 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
196 194 195 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
197 naddcom ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
198 32 100 197 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
199 117 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
200 198 199 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
201 naddcl ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
202 32 27 201 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On
203 naddcl ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
204 32 100 203 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On
205 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
206 40 32 205 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On
207 onunel ⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
208 202 204 206 207 mp3an ⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
209 196 200 208 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
210 elun1 ⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
211 209 210 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
212 189 190 191 192 211 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑌 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) ) )
213 212 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
214 188 213 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) )
215 breq12 ⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
216 214 215 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
217 216 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
218 183 217 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
219 reeanv ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
220 52 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
221 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
222 20 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 ∈ No )
223 131 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
224 23 a1i ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 0s ∈ No )
225 30 uneq2i ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) )
226 naddword1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
227 27 135 226 mp2an ⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
228 ssequn2 ⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
229 227 228 mpbi ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
230 225 229 eqtri ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
231 naddel1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) )
232 27 40 135 231 mp3an ⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
233 43 232 sylib ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
234 233 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
235 148 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
236 ontr1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
237 206 236 ax-mp ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
238 234 235 237 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
239 elun1 ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
240 238 239 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
241 230 240 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
242 221 222 223 224 241 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
243 242 simpld ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) ∈ No )
244 154 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
245 rightval ⊢ ( R ‘ 𝑌 ) = { 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑌 <s 𝑠 }
246 245 reqabi ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) ↔ ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑌 <s 𝑠 ) )
247 246 simprbi ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑌 <s 𝑠 )
248 247 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 <s 𝑠 )
249 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 ∈ No )
250 46 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
251 naddcl ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
252 27 32 251 mp2an ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On
253 naddcl ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
254 27 135 253 mp2an ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On
255 onunel ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
256 252 254 206 255 mp3an ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
257 250 238 256 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
258 elun1 ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
259 257 258 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
260 221 222 249 223 259 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) ) )
261 260 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) )
262 248 261 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) )
263 222 249 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) = ( 𝑌 +s 𝑙 ) )
264 222 223 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) = ( 𝑠 +s 𝑙 ) )
265 262 263 264 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑙 +s 𝑠 ) )
266 leftval ⊢ ( L ‘ 𝑋 ) = { 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑙 <s 𝑋 }
267 266 reqabi ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑙 <s 𝑋 ) )
268 267 simprbi ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 <s 𝑋 )
269 268 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 <s 𝑋 )
270 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
271 naddcom ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
272 135 27 271 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
273 272 238 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
274 naddcom ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
275 135 40 274 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
276 275 235 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
277 naddcl ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
278 135 27 277 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On
279 naddcl ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
280 135 40 279 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On
281 onunel ⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
282 278 280 206 281 mp3an ⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
283 273 276 282 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
284 elun1 ⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
285 283 284 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
286 221 223 222 270 285 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑠 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) ) )
287 286 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) )
288 269 287 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) )
289 220 243 244 265 288 slttrd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) )
290 breq12 ⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) ) )
291 289 290 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
292 291 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
293 219 292 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
294 218 293 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
295 reeanv ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
296 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
297 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 ∈ No )
298 60 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ No )
299 23 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 0s ∈ No )
300 81 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
301 300 83 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
302 73 301 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
303 296 297 298 299 302 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
304 303 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
305 95 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
306 103 uneq2i ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) )
307 naddword1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
308 100 68 307 mp2an ⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
309 ssequn2 ⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
310 308 309 mpbi ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
311 306 310 eqtri ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
312 naddel1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ) )
313 100 40 68 312 mp3an ⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
314 114 313 sylib ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
315 314 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
316 ontr1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
317 206 316 ax-mp ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
318 315 300 317 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
319 elun1 ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
320 318 319 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
321 311 320 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
322 296 305 298 299 321 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
323 322 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) ∈ No )
324 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
325 117 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
326 325 119 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
327 109 326 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
328 296 305 324 299 327 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
329 328 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
330 rightval ⊢ ( R ‘ 𝑋 ) = { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 }
331 330 eleq2i ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) ↔ 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
332 331 biimpi ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
333 332 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
334 rabid ⊢ ( 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } ↔ ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
335 333 334 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
336 335 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 <s 𝑟 )
337 naddcom ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
338 68 40 337 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
339 338 300 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
340 naddcom ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
341 68 100 340 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
342 341 318 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
343 naddcl ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
344 68 40 343 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On
345 naddcl ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
346 68 100 345 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On
347 onunel ⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
348 344 346 206 347 mp3an ⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
349 339 342 348 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
350 elun1 ⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
351 349 350 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
352 296 298 297 305 351 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑚 +s 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) ) )
353 352 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) )
354 336 353 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) )
355 leftval ⊢ ( L ‘ 𝑌 ) = { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 }
356 355 eleq2i ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) ↔ 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
357 356 biimpi ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
358 357 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
359 rabid ⊢ ( 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } ↔ ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
360 358 359 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
361 360 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 <s 𝑌 )
362 naddcl ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
363 100 68 362 mp2an ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On
364 naddcl ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
365 100 32 364 mp2an ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On
366 onunel ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
367 363 365 206 366 mp3an ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
368 318 325 367 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
369 elun1 ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
370 368 369 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
371 296 305 298 324 370 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) ) )
372 371 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) )
373 361 372 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) )
374 305 298 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) = ( 𝑚 +s 𝑟 ) )
375 305 324 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) = ( 𝑌 +s 𝑟 ) )
376 373 374 375 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
377 304 323 329 354 376 slttrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
378 breq12 ⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) ) )
379 377 378 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
380 379 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
381 295 380 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
382 reeanv ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
383 lltropt ⊢ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 )
384 383 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
385 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ ( L ‘ 𝑌 ) )
386 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ ( R ‘ 𝑌 ) )
387 384 385 386 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 <s 𝑠 )
388 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
389 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
390 60 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ No )
391 131 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
392 81 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
393 148 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
394 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
395 40 68 394 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On
396 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
397 40 135 396 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On
398 onunel ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
399 395 397 206 398 mp3an ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
400 392 393 399 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
401 elun1 ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
402 400 401 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
403 388 389 390 391 402 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) ) )
404 403 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) )
405 387 404 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) )
406 389 390 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) = ( 𝑚 +s 𝑋 ) )
407 389 391 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) = ( 𝑠 +s 𝑋 ) )
408 405 406 407 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) )
409 breq12 ⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) ) )
410 408 409 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
411 410 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
412 382 411 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
413 381 412 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
414 294 413 jaod ⊢ ( 𝜑 → ( ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) → 𝑎 <s 𝑏 ) )
415 182 414 biimtrid ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 ) )
416 415 3impib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 )
417 10 17 92 159 416 ssltd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )