MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsproplem2 Structured version   Visualization version   GIF version

Theorem addsproplem2 27285
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.)
Hypotheses
Ref Expression
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
Ref Expression
addsproplem2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Distinct variable groups:   𝑋,𝑙,𝑚   𝑋,𝑝,𝑞,𝑟   𝑋,𝑠,𝑡,𝑟   𝑤,𝑋   𝑥,𝑋,𝑦,𝑧   𝑌,𝑙,𝑚   𝑌,𝑝,𝑞,𝑟   𝑌,𝑠,𝑡   𝑤,𝑌   𝑥,𝑌,𝑦,𝑧   𝑥,𝑍,𝑦,𝑧   𝜑,𝑙,𝑚   𝜑,𝑝,𝑞,𝑟   𝜑,𝑠,𝑡   𝑝,𝑙,𝑟   𝑠,𝑙,𝑥,𝑦,𝑧   𝑚,𝑞,𝑟,𝑠   𝑥,𝑚,𝑦,𝑧   𝜑,𝑤,𝑟   𝑥,𝑟,𝑦,𝑧,𝑠   𝑞,𝑙   𝑟,𝑝,𝑞   𝑤,𝑝   𝑠,𝑞,𝑡
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝑍(𝑤,𝑡,𝑚,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem addsproplem2
Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvex 6856 . . . . 5 ( L ‘𝑋) ∈ V
21abrexex 7896 . . . 4 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V
32a1i 11 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V)
4 fvex 6856 . . . . 5 ( L ‘𝑌) ∈ V
54abrexex 7896 . . . 4 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V
65a1i 11 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V)
73, 6unexd 7689 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V)
8 fvex 6856 . . . . 5 ( R ‘𝑋) ∈ V
98abrexex 7896 . . . 4 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V
109a1i 11 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V)
11 fvex 6856 . . . . 5 ( R ‘𝑌) ∈ V
1211abrexex 7896 . . . 4 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V
1312a1i 11 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V)
1410, 13unexd 7689 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ∈ V)
15 addsproplem.1 . . . . . . . . 9 (𝜑 → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
1615adantr 482 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
17 leftssno 27213 . . . . . . . . . 10 ( L ‘𝑋) ⊆ No
1817sseli 3941 . . . . . . . . 9 (𝑙 ∈ ( L ‘𝑋) → 𝑙 No )
1918adantl 483 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑙 No )
20 addsproplem2.3 . . . . . . . . 9 (𝜑𝑌 No )
2120adantr 482 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑌 No )
22 0sno 27168 . . . . . . . . 9 0s No
2322a1i 11 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 0s No )
24 bday0s 27170 . . . . . . . . . . . . 13 ( bday ‘ 0s ) = ∅
2524oveq2i 7369 . . . . . . . . . . . 12 (( bday 𝑙) +no ( bday ‘ 0s )) = (( bday 𝑙) +no ∅)
26 bdayelon 27119 . . . . . . . . . . . . 13 ( bday 𝑙) ∈ On
27 naddid1 8630 . . . . . . . . . . . . 13 (( bday 𝑙) ∈ On → (( bday 𝑙) +no ∅) = ( bday 𝑙))
2826, 27ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑙) +no ∅) = ( bday 𝑙)
2925, 28eqtri 2765 . . . . . . . . . . 11 (( bday 𝑙) +no ( bday ‘ 0s )) = ( bday 𝑙)
3029uneq2i 4121 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙))
31 bdayelon 27119 . . . . . . . . . . . 12 ( bday 𝑌) ∈ On
32 naddword1 8637 . . . . . . . . . . . 12 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)))
3326, 31, 32mp2an 691 . . . . . . . . . . 11 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌))
34 ssequn2 4144 . . . . . . . . . . 11 (( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)) ↔ ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌)))
3533, 34mpbi 229 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌))
3630, 35eqtri 2765 . . . . . . . . 9 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑌))
37 leftssold 27211 . . . . . . . . . . . . . 14 ( L ‘𝑋) ⊆ ( O ‘( bday 𝑋))
3837sseli 3941 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday 𝑋)))
39 bdayelon 27119 . . . . . . . . . . . . . 14 ( bday 𝑋) ∈ On
40 oldbday 27233 . . . . . . . . . . . . . 14 ((( bday 𝑋) ∈ On ∧ 𝑙 No ) → (𝑙 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑙) ∈ ( bday 𝑋)))
4139, 18, 40sylancr 588 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑙) ∈ ( bday 𝑋)))
4238, 41mpbid 231 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → ( bday 𝑙) ∈ ( bday 𝑋))
43 naddel1 8633 . . . . . . . . . . . . 13 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
4426, 39, 31, 43mp3an 1462 . . . . . . . . . . . 12 (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
4542, 44sylib 217 . . . . . . . . . . 11 (𝑙 ∈ ( L ‘𝑋) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
4645adantl 483 . . . . . . . . . 10 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
47 elun1 4137 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑙) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
4846, 47syl 17 . . . . . . . . 9 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (( bday 𝑙) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
4936, 48eqeltrid 2842 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
5016, 19, 21, 23, 49addsproplem1 27284 . . . . . . 7 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑙) <s ( 0s +s 𝑙))))
5150simpld 496 . . . . . 6 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No )
52 eleq1a 2833 . . . . . 6 ((𝑙 +s 𝑌) ∈ No → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5351, 52syl 17 . . . . 5 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5453rexlimdva 3153 . . . 4 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5554abssdv 4026 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ⊆ No )
5615adantr 482 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
57 addsproplem2.2 . . . . . . . . 9 (𝜑𝑋 No )
5857adantr 482 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 𝑋 No )
59 leftssno 27213 . . . . . . . . . 10 ( L ‘𝑌) ⊆ No
6059sseli 3941 . . . . . . . . 9 (𝑚 ∈ ( L ‘𝑌) → 𝑚 No )
6160adantl 483 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 𝑚 No )
6222a1i 11 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 0s No )
6324oveq2i 7369 . . . . . . . . . . . 12 (( bday 𝑋) +no ( bday ‘ 0s )) = (( bday 𝑋) +no ∅)
64 naddid1 8630 . . . . . . . . . . . . 13 (( bday 𝑋) ∈ On → (( bday 𝑋) +no ∅) = ( bday 𝑋))
6539, 64ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑋) +no ∅) = ( bday 𝑋)
6663, 65eqtri 2765 . . . . . . . . . . 11 (( bday 𝑋) +no ( bday ‘ 0s )) = ( bday 𝑋)
6766uneq2i 4121 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋))
68 bdayelon 27119 . . . . . . . . . . . 12 ( bday 𝑚) ∈ On
69 naddword1 8637 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)))
7039, 68, 69mp2an 691 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚))
71 ssequn2 4144 . . . . . . . . . . 11 (( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)) ↔ ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
7270, 71mpbi 229 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
7367, 72eqtri 2765 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑚))
74 leftssold 27211 . . . . . . . . . . . . . 14 ( L ‘𝑌) ⊆ ( O ‘( bday 𝑌))
7574sseli 3941 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday 𝑌)))
76 oldbday 27233 . . . . . . . . . . . . . 14 ((( bday 𝑌) ∈ On ∧ 𝑚 No ) → (𝑚 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑚) ∈ ( bday 𝑌)))
7731, 60, 76sylancr 588 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑚) ∈ ( bday 𝑌)))
7875, 77mpbid 231 . . . . . . . . . . . 12 (𝑚 ∈ ( L ‘𝑌) → ( bday 𝑚) ∈ ( bday 𝑌))
79 naddel2 8634 . . . . . . . . . . . . 13 ((( bday 𝑚) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
8068, 31, 39, 79mp3an 1462 . . . . . . . . . . . 12 (( bday 𝑚) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
8178, 80sylib 217 . . . . . . . . . . 11 (𝑚 ∈ ( L ‘𝑌) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
8281adantl 483 . . . . . . . . . 10 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
83 elun1 4137 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑋) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8482, 83syl 17 . . . . . . . . 9 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8573, 84eqeltrid 2842 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8656, 58, 61, 62, 85addsproplem1 27284 . . . . . . 7 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
8786simpld 496 . . . . . 6 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No )
88 eleq1a 2833 . . . . . 6 ((𝑋 +s 𝑚) ∈ No → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
8987, 88syl 17 . . . . 5 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9089rexlimdva 3153 . . . 4 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9190abssdv 4026 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No )
9255, 91unssd 4147 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ⊆ No )
9315adantr 482 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
94 rightssno 27214 . . . . . . . . . 10 ( R ‘𝑋) ⊆ No
9594sseli 3941 . . . . . . . . 9 (𝑟 ∈ ( R ‘𝑋) → 𝑟 No )
9695adantl 483 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑟 No )
9720adantr 482 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑌 No )
9822a1i 11 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 0s No )
9924oveq2i 7369 . . . . . . . . . . . 12 (( bday 𝑟) +no ( bday ‘ 0s )) = (( bday 𝑟) +no ∅)
100 bdayelon 27119 . . . . . . . . . . . . 13 ( bday 𝑟) ∈ On
101 naddid1 8630 . . . . . . . . . . . . 13 (( bday 𝑟) ∈ On → (( bday 𝑟) +no ∅) = ( bday 𝑟))
102100, 101ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑟) +no ∅) = ( bday 𝑟)
10399, 102eqtri 2765 . . . . . . . . . . 11 (( bday 𝑟) +no ( bday ‘ 0s )) = ( bday 𝑟)
104103uneq2i 4121 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟))
105 naddword1 8637 . . . . . . . . . . . 12 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)))
106100, 31, 105mp2an 691 . . . . . . . . . . 11 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌))
107 ssequn2 4144 . . . . . . . . . . 11 (( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)) ↔ ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌)))
108106, 107mpbi 229 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌))
109104, 108eqtri 2765 . . . . . . . . 9 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑌))
110 rightssold 27212 . . . . . . . . . . . . . 14 ( R ‘𝑋) ⊆ ( O ‘( bday 𝑋))
111110sseli 3941 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday 𝑋)))
112 oldbday 27233 . . . . . . . . . . . . . 14 ((( bday 𝑋) ∈ On ∧ 𝑟 No ) → (𝑟 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑟) ∈ ( bday 𝑋)))
11339, 95, 112sylancr 588 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑟) ∈ ( bday 𝑋)))
114111, 113mpbid 231 . . . . . . . . . . . 12 (𝑟 ∈ ( R ‘𝑋) → ( bday 𝑟) ∈ ( bday 𝑋))
115 naddel1 8633 . . . . . . . . . . . . 13 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
116100, 39, 31, 115mp3an 1462 . . . . . . . . . . . 12 (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
117114, 116sylib 217 . . . . . . . . . . 11 (𝑟 ∈ ( R ‘𝑋) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
118117adantl 483 . . . . . . . . . 10 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
119 elun1 4137 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑟) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
120118, 119syl 17 . . . . . . . . 9 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (( bday 𝑟) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
121109, 120eqeltrid 2842 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
12293, 96, 97, 98, 121addsproplem1 27284 . . . . . . 7 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
123122simpld 496 . . . . . 6 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No )
124 eleq1a 2833 . . . . . 6 ((𝑟 +s 𝑌) ∈ No → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
125123, 124syl 17 . . . . 5 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
126125rexlimdva 3153 . . . 4 (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
127126abssdv 4026 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ⊆ No )
12815adantr 482 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
12957adantr 482 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑋 No )
130 rightssno 27214 . . . . . . . . . 10 ( R ‘𝑌) ⊆ No
131130sseli 3941 . . . . . . . . 9 (𝑠 ∈ ( R ‘𝑌) → 𝑠 No )
132131adantl 483 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑠 No )
13322a1i 11 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 0s No )
13466uneq2i 4121 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋))
135 bdayelon 27119 . . . . . . . . . . . 12 ( bday 𝑠) ∈ On
136 naddword1 8637 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)))
13739, 135, 136mp2an 691 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠))
138 ssequn2 4144 . . . . . . . . . . 11 (( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)) ↔ ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
139137, 138mpbi 229 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
140134, 139eqtri 2765 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑠))
141 rightssold 27212 . . . . . . . . . . . . . 14 ( R ‘𝑌) ⊆ ( O ‘( bday 𝑌))
142141sseli 3941 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday 𝑌)))
143 oldbday 27233 . . . . . . . . . . . . . 14 ((( bday 𝑌) ∈ On ∧ 𝑠 No ) → (𝑠 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑠) ∈ ( bday 𝑌)))
14431, 131, 143sylancr 588 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑠) ∈ ( bday 𝑌)))
145142, 144mpbid 231 . . . . . . . . . . . 12 (𝑠 ∈ ( R ‘𝑌) → ( bday 𝑠) ∈ ( bday 𝑌))
146 naddel2 8634 . . . . . . . . . . . . 13 ((( bday 𝑠) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
147135, 31, 39, 146mp3an 1462 . . . . . . . . . . . 12 (( bday 𝑠) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
148145, 147sylib 217 . . . . . . . . . . 11 (𝑠 ∈ ( R ‘𝑌) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
149148adantl 483 . . . . . . . . . 10 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
150 elun1 4137 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑋) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
151149, 150syl 17 . . . . . . . . 9 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
152140, 151eqeltrid 2842 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
153128, 129, 132, 133, 152addsproplem1 27284 . . . . . . 7 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑋) <s ( 0s +s 𝑋))))
154153simpld 496 . . . . . 6 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No )
155 eleq1a 2833 . . . . . 6 ((𝑋 +s 𝑠) ∈ No → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
156154, 155syl 17 . . . . 5 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
157156rexlimdva 3153 . . . 4 (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
158157abssdv 4026 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No )
159127, 158unssd 4147 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No )
160 elun 4109 . . . . . . 7 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}))
161 vex 3450 . . . . . . . . 9 𝑎 ∈ V
162 eqeq1 2741 . . . . . . . . . 10 (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌)))
163162rexbidv 3176 . . . . . . . . 9 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)))
164161, 163elab 3631 . . . . . . . 8 (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))
165 eqeq1 2741 . . . . . . . . . 10 (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚)))
166165rexbidv 3176 . . . . . . . . 9 (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
167161, 166elab 3631 . . . . . . . 8 (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))
168164, 167orbi12i 914 . . . . . . 7 ((𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
169160, 168bitri 275 . . . . . 6 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
170 elun 4109 . . . . . . 7 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
171 vex 3450 . . . . . . . . 9 𝑏 ∈ V
172 eqeq1 2741 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌)))
173172rexbidv 3176 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
174171, 173elab 3631 . . . . . . . 8 (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))
175 eqeq1 2741 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠)))
176175rexbidv 3176 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
177171, 176elab 3631 . . . . . . . 8 (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))
178174, 177orbi12i 914 . . . . . . 7 ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
179170, 178bitri 275 . . . . . 6 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
180169, 179anbi12i 628 . . . . 5 ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) ↔ ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))))
181 anddi 1010 . . . . 5 (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ↔ (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))))
182180, 181bitri 275 . . . 4 ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( 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 3218 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
184 lltropt 27205 . . . . . . . . . . . . 13 (𝑋 No → ( L ‘𝑋) <<s ( R ‘𝑋))
18557, 184syl 17 . . . . . . . . . . . 12 (𝜑 → ( L ‘𝑋) <<s ( R ‘𝑋))
186185adantr 482 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
187 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
188 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
189186, 187, 188ssltsepcd 27136 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟)
19015adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
19120adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
19218ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 No )
19395ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
194 naddcom 8629 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌)))
19531, 26, 194mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌))
19645ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
197195, 196eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
198 naddcom 8629 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌)))
19931, 100, 198mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌))
200117ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
201199, 200eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
202 naddcl 8624 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) ∈ On)
20331, 26, 202mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) ∈ On
204 naddcl 8624 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) ∈ On)
20531, 100, 204mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) ∈ On
206 naddcl 8624 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑋) +no ( bday 𝑌)) ∈ On)
20739, 31, 206mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑋) +no ( bday 𝑌)) ∈ On
208 onunel 6423 . . . . . . . . . . . . . . 15 (((( 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 𝑌)))))
209203, 205, 207, 208mp3an 1462 . . . . . . . . . . . . . 14 (((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
210197, 201, 209sylanbrc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
211 elun1 4137 . . . . . . . . . . . . 13 (((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
212210, 211syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
213190, 191, 192, 193, 212addsproplem1 27284 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))))
214213simprd 497 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
215189, 214mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))
216 breq12 5111 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
217215, 216syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
218217rexlimdvva 3206 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
219183, 218biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
220 reeanv 3218 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
22151adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No )
22215adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
22318ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 No )
224131ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
22522a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s No )
22629uneq2i 4121 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙))
227 naddword1 8637 . . . . . . . . . . . . . . . 16 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)))
22826, 135, 227mp2an 691 . . . . . . . . . . . . . . 15 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠))
229 ssequn2 4144 . . . . . . . . . . . . . . 15 (( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)) ↔ ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
230228, 229mpbi 229 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
231226, 230eqtri 2765 . . . . . . . . . . . . 13 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑠))
232 naddel1 8633 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠))))
23326, 39, 135, 232mp3an 1462 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
23442, 233sylib 217 . . . . . . . . . . . . . . . 16 (𝑙 ∈ ( L ‘𝑋) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
235234ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
236148ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
237 ontr1 6364 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) +no ( bday 𝑌)) ∈ On → (((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
238207, 237ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
239235, 236, 238syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
240 elun1 4137 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑙) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
241239, 240syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
242231, 241eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
243222, 223, 224, 225, 242addsproplem1 27284 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑙) <s ( 0s +s 𝑙))))
244243simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No )
245154adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No )
246 rightval 27197 . . . . . . . . . . . . . . 15 ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday 𝑌)) ∣ 𝑌 <s 𝑠}
247246reqabi 3430 . . . . . . . . . . . . . 14 (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘( bday 𝑌)) ∧ 𝑌 <s 𝑠))
248247simprbi 498 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
249248ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
25020adantr 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 No )
25145ad2antrl 727 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
252 naddcl 8624 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) +no ( bday 𝑌)) ∈ On)
25326, 31, 252mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑌)) ∈ On
254 naddcl 8624 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) +no ( bday 𝑠)) ∈ On)
25526, 135, 254mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑠)) ∈ On
256 onunel 6423 . . . . . . . . . . . . . . . . 17 (((( 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 𝑌)))))
257253, 255, 207, 256mp3an 1462 . . . . . . . . . . . . . . . 16 (((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
258251, 239, 257sylanbrc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
259 elun1 4137 . . . . . . . . . . . . . . 15 (((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
260258, 259syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
261222, 223, 250, 224, 260addsproplem1 27284 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))))
262261simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))
263249, 262mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))
264223, 250addscomd 27282 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙))
265223, 224addscomd 27282 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙))
266263, 264, 2653brtr4d 5138 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠))
267 leftval 27196 . . . . . . . . . . . . . 14 ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday 𝑋)) ∣ 𝑙 <s 𝑋}
268267reqabi 3430 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday 𝑋)) ∧ 𝑙 <s 𝑋))
269268simprbi 498 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
270269ad2antrl 727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
27157adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
272 naddcom 8629 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
273135, 26, 272mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
274273, 239eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
275 naddcom 8629 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
276135, 39, 275mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
277276, 236eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
278 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) ∈ On)
279135, 26, 278mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) ∈ On
280 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) ∈ On)
281135, 39, 280mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) ∈ On
282 onunel 6423 . . . . . . . . . . . . . . . 16 (((( 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 𝑌)))))
283279, 281, 207, 282mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
284274, 277, 283sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
285 elun1 4137 . . . . . . . . . . . . . 14 (((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
286284, 285syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
287222, 224, 223, 271, 286addsproplem1 27284 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))))
288287simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))
289270, 288mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))
290221, 244, 245, 266, 289slttrd 27110 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))
291 breq12 5111 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)))
292290, 291syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
293292rexlimdvva 3206 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
294220, 293biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
295219, 294jaod 858 . . . . 5 (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
296 reeanv 3218 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
29715adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
29857adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 No )
29960ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 No )
30022a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s No )
30181ad2antrl 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
302301, 83syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
30373, 302eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
304297, 298, 299, 300, 303addsproplem1 27284 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
305304simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No )
30695ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
307103uneq2i 4121 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟))
308 naddword1 8637 . . . . . . . . . . . . . . . 16 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)))
309100, 68, 308mp2an 691 . . . . . . . . . . . . . . 15 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚))
310 ssequn2 4144 . . . . . . . . . . . . . . 15 (( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)) ↔ ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
311309, 310mpbi 229 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
312307, 311eqtri 2765 . . . . . . . . . . . . 13 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑚))
313 naddel1 8633 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚))))
314100, 39, 68, 313mp3an 1462 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
315114, 314sylib 217 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ( R ‘𝑋) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
316315ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
317 ontr1 6364 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) +no ( bday 𝑌)) ∈ On → (((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)) ∧ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
318207, 317ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)) ∧ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
319316, 301, 318syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
320 elun1 4137 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑟) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
321319, 320syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
322312, 321eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
323297, 306, 299, 300, 322addsproplem1 27284 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑟) <s ( 0s +s 𝑟))))
324323simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No )
32520adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
326117ad2antll 728 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
327326, 119syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
328109, 327eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
329297, 306, 325, 300, 328addsproplem1 27284 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
330329simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No )
331 rightval 27197 . . . . . . . . . . . . . . . 16 ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟}
332331eleq2i 2830 . . . . . . . . . . . . . . 15 (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
333332biimpi 215 . . . . . . . . . . . . . 14 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
334333ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
335 rabid 3428 . . . . . . . . . . . . 13 (𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
336334, 335sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
337336simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
338 naddcom 8629 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
33968, 39, 338mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
340339, 301eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
341 naddcom 8629 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
34268, 100, 341mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
343342, 319eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
344 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) ∈ On)
34568, 39, 344mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) ∈ On
346 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) ∈ On)
34768, 100, 346mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) ∈ On
348 onunel 6423 . . . . . . . . . . . . . . . 16 (((( 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 𝑌)))))
349345, 347, 207, 348mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
350340, 343, 349sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
351 elun1 4137 . . . . . . . . . . . . . 14 (((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
352350, 351syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
353297, 299, 298, 306, 352addsproplem1 27284 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No ∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))))
354353simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))
355337, 354mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))
356 leftval 27196 . . . . . . . . . . . . . . . . 17 ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌}
357356eleq2i 2830 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
358357biimpi 215 . . . . . . . . . . . . . . 15 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
359358ad2antrl 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
360 rabid 3428 . . . . . . . . . . . . . 14 (𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
361359, 360sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
362361simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
363 naddcl 8624 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) +no ( bday 𝑚)) ∈ On)
364100, 68, 363mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑚)) ∈ On
365 naddcl 8624 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) +no ( bday 𝑌)) ∈ On)
366100, 31, 365mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑌)) ∈ On
367 onunel 6423 . . . . . . . . . . . . . . . . 17 (((( 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 𝑌)))))
368364, 366, 207, 367mp3an 1462 . . . . . . . . . . . . . . . 16 (((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
369319, 326, 368sylanbrc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
370 elun1 4137 . . . . . . . . . . . . . . 15 (((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
371369, 370syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
372297, 306, 299, 325, 371addsproplem1 27284 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))))
373372simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))
374362, 373mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))
375306, 299addscomd 27282 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟))
376306, 325addscomd 27282 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟))
377374, 375, 3763brtr4d 5138 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌))
378305, 324, 330, 355, 377slttrd 27110 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))
379 breq12 5111 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)))
380378, 379syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
381380rexlimdvva 3206 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
382296, 381biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
383 reeanv 3218 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
384 lltropt 27205 . . . . . . . . . . . . . 14 (𝑌 No → ( L ‘𝑌) <<s ( R ‘𝑌))
38520, 384syl 17 . . . . . . . . . . . . 13 (𝜑 → ( L ‘𝑌) <<s ( R ‘𝑌))
386385adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
387 simprl 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
388 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
389386, 387, 388ssltsepcd 27136 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠)
39015adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
39157adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
39260ad2antrl 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 No )
393131ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
39481ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
395148ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
396 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑋) +no ( bday 𝑚)) ∈ On)
39739, 68, 396mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑚)) ∈ On
398 naddcl 8624 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑋) +no ( bday 𝑠)) ∈ On)
39939, 135, 398mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑠)) ∈ On
400 onunel 6423 . . . . . . . . . . . . . . . 16 (((( 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 𝑌)))))
401397, 399, 207, 400mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
402394, 395, 401sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
403 elun1 4137 . . . . . . . . . . . . . 14 (((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
404402, 403syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
405390, 391, 392, 393, 404addsproplem1 27284 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))))
406405simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))
407389, 406mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))
408391, 392addscomd 27282 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋))
409391, 393addscomd 27282 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋))
410407, 408, 4093brtr4d 5138 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))
411 breq12 5111 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)))
412410, 411syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
413412rexlimdvva 3206 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
414383, 413biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
415382, 414jaod 858 . . . . 5 (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
416295, 415jaod 858 . . . 4 (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏))
417182, 416biimtrid 241 . . 3 (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏))
4184173impib 1117 . 2 ((𝜑𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)
4197, 14, 92, 159, 418ssltd 27134 1 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wo 846   = wceq 1542  wcel 2107  {cab 2714  wral 3065  wrex 3074  {crab 3408  Vcvv 3446  cun 3909  wss 3911  c0 4283   class class class wbr 5106  Oncon0 6318  cfv 6497  (class class class)co 7358   +no cnadd 8612   No csur 26991   <s cslt 26992   bday cbday 26993   <<s csslt 27123   0s c0s 27164   O cold 27176   L cleft 27178   R cright 27179   +s cadds 27274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-1o 8413  df-2o 8414  df-nadd 8613  df-no 26994  df-slt 26995  df-bday 26996  df-sslt 27124  df-scut 27126  df-0s 27166  df-made 27180  df-old 27181  df-left 27183  df-right 27184  df-norec2 27264  df-adds 27275
This theorem is referenced by:  addsproplem3  27286
  Copyright terms: Public domain W3C validator