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

Theorem addsproplem2 27444
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 6902 . . . . 5 ( L ‘𝑋) ∈ V
21abrexex 7946 . . . 4 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V
32a1i 11 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V)
4 fvex 6902 . . . . 5 ( L ‘𝑌) ∈ V
54abrexex 7946 . . . 4 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V
65a1i 11 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V)
73, 6unexd 7738 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V)
8 fvex 6902 . . . . 5 ( R ‘𝑋) ∈ V
98abrexex 7946 . . . 4 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V
109a1i 11 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V)
11 fvex 6902 . . . . 5 ( R ‘𝑌) ∈ V
1211abrexex 7946 . . . 4 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V
1312a1i 11 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V)
1410, 13unexd 7738 . 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 27365 . . . . . . . . . 10 ( L ‘𝑋) ⊆ No
1817sseli 3978 . . . . . . . . 9 (𝑙 ∈ ( L ‘𝑋) → 𝑙 No )
1918adantl 483 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑙 No )
20 addsproplem2.3 . . . . . . . . 9 (𝜑𝑌 No )
2120adantr 482 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑌 No )
22 0sno 27317 . . . . . . . . 9 0s No
2322a1i 11 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 0s No )
24 bday0s 27319 . . . . . . . . . . . . 13 ( bday ‘ 0s ) = ∅
2524oveq2i 7417 . . . . . . . . . . . 12 (( bday 𝑙) +no ( bday ‘ 0s )) = (( bday 𝑙) +no ∅)
26 bdayelon 27268 . . . . . . . . . . . . 13 ( bday 𝑙) ∈ On
27 naddrid 8679 . . . . . . . . . . . . 13 (( bday 𝑙) ∈ On → (( bday 𝑙) +no ∅) = ( bday 𝑙))
2826, 27ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑙) +no ∅) = ( bday 𝑙)
2925, 28eqtri 2761 . . . . . . . . . . 11 (( bday 𝑙) +no ( bday ‘ 0s )) = ( bday 𝑙)
3029uneq2i 4160 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙))
31 bdayelon 27268 . . . . . . . . . . . 12 ( bday 𝑌) ∈ On
32 naddword1 8687 . . . . . . . . . . . 12 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)))
3326, 31, 32mp2an 691 . . . . . . . . . . 11 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌))
34 ssequn2 4183 . . . . . . . . . . 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 2761 . . . . . . . . 9 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑌))
37 leftssold 27363 . . . . . . . . . . . . . 14 ( L ‘𝑋) ⊆ ( O ‘( bday 𝑋))
3837sseli 3978 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday 𝑋)))
39 bdayelon 27268 . . . . . . . . . . . . . 14 ( bday 𝑋) ∈ On
40 oldbday 27385 . . . . . . . . . . . . . 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 8683 . . . . . . . . . . . . 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 4176 . . . . . . . . . 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 2838 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
5016, 19, 21, 23, 49addsproplem1 27443 . . . . . . 7 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑙) <s ( 0s +s 𝑙))))
5150simpld 496 . . . . . 6 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No )
52 eleq1a 2829 . . . . . 6 ((𝑙 +s 𝑌) ∈ No → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5351, 52syl 17 . . . . 5 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5453rexlimdva 3156 . . . 4 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5554abssdv 4065 . . 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 27365 . . . . . . . . . 10 ( L ‘𝑌) ⊆ No
6059sseli 3978 . . . . . . . . 9 (𝑚 ∈ ( L ‘𝑌) → 𝑚 No )
6160adantl 483 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 𝑚 No )
6222a1i 11 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 0s No )
6324oveq2i 7417 . . . . . . . . . . . 12 (( bday 𝑋) +no ( bday ‘ 0s )) = (( bday 𝑋) +no ∅)
64 naddrid 8679 . . . . . . . . . . . . 13 (( bday 𝑋) ∈ On → (( bday 𝑋) +no ∅) = ( bday 𝑋))
6539, 64ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑋) +no ∅) = ( bday 𝑋)
6663, 65eqtri 2761 . . . . . . . . . . 11 (( bday 𝑋) +no ( bday ‘ 0s )) = ( bday 𝑋)
6766uneq2i 4160 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋))
68 bdayelon 27268 . . . . . . . . . . . 12 ( bday 𝑚) ∈ On
69 naddword1 8687 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)))
7039, 68, 69mp2an 691 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚))
71 ssequn2 4183 . . . . . . . . . . 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 2761 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑚))
74 leftssold 27363 . . . . . . . . . . . . . 14 ( L ‘𝑌) ⊆ ( O ‘( bday 𝑌))
7574sseli 3978 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday 𝑌)))
76 oldbday 27385 . . . . . . . . . . . . . 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 8684 . . . . . . . . . . . . 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 4176 . . . . . . . . . 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 2838 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8656, 58, 61, 62, 85addsproplem1 27443 . . . . . . 7 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
8786simpld 496 . . . . . 6 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No )
88 eleq1a 2829 . . . . . 6 ((𝑋 +s 𝑚) ∈ No → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
8987, 88syl 17 . . . . 5 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9089rexlimdva 3156 . . . 4 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9190abssdv 4065 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No )
9255, 91unssd 4186 . 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 27366 . . . . . . . . . 10 ( R ‘𝑋) ⊆ No
9594sseli 3978 . . . . . . . . 9 (𝑟 ∈ ( R ‘𝑋) → 𝑟 No )
9695adantl 483 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑟 No )
9720adantr 482 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑌 No )
9822a1i 11 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 0s No )
9924oveq2i 7417 . . . . . . . . . . . 12 (( bday 𝑟) +no ( bday ‘ 0s )) = (( bday 𝑟) +no ∅)
100 bdayelon 27268 . . . . . . . . . . . . 13 ( bday 𝑟) ∈ On
101 naddrid 8679 . . . . . . . . . . . . 13 (( bday 𝑟) ∈ On → (( bday 𝑟) +no ∅) = ( bday 𝑟))
102100, 101ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑟) +no ∅) = ( bday 𝑟)
10399, 102eqtri 2761 . . . . . . . . . . 11 (( bday 𝑟) +no ( bday ‘ 0s )) = ( bday 𝑟)
104103uneq2i 4160 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟))
105 naddword1 8687 . . . . . . . . . . . 12 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)))
106100, 31, 105mp2an 691 . . . . . . . . . . 11 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌))
107 ssequn2 4183 . . . . . . . . . . 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 2761 . . . . . . . . 9 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑌))
110 rightssold 27364 . . . . . . . . . . . . . 14 ( R ‘𝑋) ⊆ ( O ‘( bday 𝑋))
111110sseli 3978 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday 𝑋)))
112 oldbday 27385 . . . . . . . . . . . . . 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 8683 . . . . . . . . . . . . 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 4176 . . . . . . . . . 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 2838 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
12293, 96, 97, 98, 121addsproplem1 27443 . . . . . . 7 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
123122simpld 496 . . . . . 6 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No )
124 eleq1a 2829 . . . . . 6 ((𝑟 +s 𝑌) ∈ No → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
125123, 124syl 17 . . . . 5 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
126125rexlimdva 3156 . . . 4 (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
127126abssdv 4065 . . 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 27366 . . . . . . . . . 10 ( R ‘𝑌) ⊆ No
131130sseli 3978 . . . . . . . . 9 (𝑠 ∈ ( R ‘𝑌) → 𝑠 No )
132131adantl 483 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑠 No )
13322a1i 11 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 0s No )
13466uneq2i 4160 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋))
135 bdayelon 27268 . . . . . . . . . . . 12 ( bday 𝑠) ∈ On
136 naddword1 8687 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)))
13739, 135, 136mp2an 691 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠))
138 ssequn2 4183 . . . . . . . . . . 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 2761 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑠))
141 rightssold 27364 . . . . . . . . . . . . . 14 ( R ‘𝑌) ⊆ ( O ‘( bday 𝑌))
142141sseli 3978 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday 𝑌)))
143 oldbday 27385 . . . . . . . . . . . . . 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 8684 . . . . . . . . . . . . 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 4176 . . . . . . . . . 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 2838 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
153128, 129, 132, 133, 152addsproplem1 27443 . . . . . . 7 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑋) <s ( 0s +s 𝑋))))
154153simpld 496 . . . . . 6 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No )
155 eleq1a 2829 . . . . . 6 ((𝑋 +s 𝑠) ∈ No → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
156154, 155syl 17 . . . . 5 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
157156rexlimdva 3156 . . . 4 (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
158157abssdv 4065 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No )
159127, 158unssd 4186 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No )
160 elun 4148 . . . . . . 7 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}))
161 vex 3479 . . . . . . . . 9 𝑎 ∈ V
162 eqeq1 2737 . . . . . . . . . 10 (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌)))
163162rexbidv 3179 . . . . . . . . 9 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)))
164161, 163elab 3668 . . . . . . . 8 (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))
165 eqeq1 2737 . . . . . . . . . 10 (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚)))
166165rexbidv 3179 . . . . . . . . 9 (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
167161, 166elab 3668 . . . . . . . 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 4148 . . . . . . 7 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
171 vex 3479 . . . . . . . . 9 𝑏 ∈ V
172 eqeq1 2737 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌)))
173172rexbidv 3179 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
174171, 173elab 3668 . . . . . . . 8 (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))
175 eqeq1 2737 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠)))
176175rexbidv 3179 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
177171, 176elab 3668 . . . . . . . 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 3227 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
184 lltropt 27357 . . . . . . . . . . . 12 ( L ‘𝑋) <<s ( R ‘𝑋)
185184a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
186 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
187 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
188185, 186, 187ssltsepcd 27285 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟)
18915adantr 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 𝑥)))))
19020adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
19118ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 No )
19295ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
193 naddcom 8678 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌)))
19431, 26, 193mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌))
19545ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
196194, 195eqeltrid 2838 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
197 naddcom 8678 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌)))
19831, 100, 197mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌))
199117ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
200198, 199eqeltrid 2838 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
201 naddcl 8673 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) ∈ On)
20231, 26, 201mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) ∈ On
203 naddcl 8673 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) ∈ On)
20431, 100, 203mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) ∈ On
205 naddcl 8673 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑋) +no ( bday 𝑌)) ∈ On)
20639, 31, 205mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑋) +no ( bday 𝑌)) ∈ On
207 onunel 6467 . . . . . . . . . . . . . . 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 𝑌)))))
208202, 204, 206, 207mp3an 1462 . . . . . . . . . . . . . 14 (((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
209196, 200, 208sylanbrc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
210 elun1 4176 . . . . . . . . . . . . 13 (((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
211209, 210syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
212189, 190, 191, 192, 211addsproplem1 27443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))))
213212simprd 497 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
214188, 213mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))
215 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
216214, 215syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
217216rexlimdvva 3212 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
218183, 217biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
219 reeanv 3227 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
22051adantrr 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No )
22115adantr 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 𝑥)))))
22218ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 No )
223131ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
22422a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s No )
22529uneq2i 4160 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙))
226 naddword1 8687 . . . . . . . . . . . . . . . 16 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)))
22726, 135, 226mp2an 691 . . . . . . . . . . . . . . 15 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠))
228 ssequn2 4183 . . . . . . . . . . . . . . 15 (( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)) ↔ ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
229227, 228mpbi 229 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
230225, 229eqtri 2761 . . . . . . . . . . . . 13 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑠))
231 naddel1 8683 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠))))
23226, 39, 135, 231mp3an 1462 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
23342, 232sylib 217 . . . . . . . . . . . . . . . 16 (𝑙 ∈ ( L ‘𝑋) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
234233ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
235148ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
236 ontr1 6408 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) +no ( bday 𝑌)) ∈ On → (((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
237206, 236ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
238234, 235, 237syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
239 elun1 4176 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑙) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
240238, 239syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
241230, 240eqeltrid 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
242221, 222, 223, 224, 241addsproplem1 27443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑙) <s ( 0s +s 𝑙))))
243242simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No )
244154adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No )
245 rightval 27349 . . . . . . . . . . . . . . 15 ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday 𝑌)) ∣ 𝑌 <s 𝑠}
246245reqabi 3455 . . . . . . . . . . . . . 14 (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘( bday 𝑌)) ∧ 𝑌 <s 𝑠))
247246simprbi 498 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
248247ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
24920adantr 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 No )
25045ad2antrl 727 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
251 naddcl 8673 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) +no ( bday 𝑌)) ∈ On)
25226, 31, 251mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑌)) ∈ On
253 naddcl 8673 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) +no ( bday 𝑠)) ∈ On)
25426, 135, 253mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑠)) ∈ On
255 onunel 6467 . . . . . . . . . . . . . . . . 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 𝑌)))))
256252, 254, 206, 255mp3an 1462 . . . . . . . . . . . . . . . 16 (((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
257250, 238, 256sylanbrc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
258 elun1 4176 . . . . . . . . . . . . . . 15 (((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
259257, 258syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
260221, 222, 249, 223, 259addsproplem1 27443 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))))
261260simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))
262248, 261mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))
263222, 249addscomd 27441 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙))
264222, 223addscomd 27441 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙))
265262, 263, 2643brtr4d 5180 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠))
266 leftval 27348 . . . . . . . . . . . . . 14 ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday 𝑋)) ∣ 𝑙 <s 𝑋}
267266reqabi 3455 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday 𝑋)) ∧ 𝑙 <s 𝑋))
268267simprbi 498 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
269268ad2antrl 727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
27057adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
271 naddcom 8678 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
272135, 26, 271mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
273272, 238eqeltrid 2838 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
274 naddcom 8678 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
275135, 39, 274mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
276275, 235eqeltrid 2838 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
277 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) ∈ On)
278135, 26, 277mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) ∈ On
279 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) ∈ On)
280135, 39, 279mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) ∈ On
281 onunel 6467 . . . . . . . . . . . . . . . 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 𝑌)))))
282278, 280, 206, 281mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
283273, 276, 282sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
284 elun1 4176 . . . . . . . . . . . . . 14 (((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
285283, 284syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
286221, 223, 222, 270, 285addsproplem1 27443 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))))
287286simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))
288269, 287mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))
289220, 243, 244, 265, 288slttrd 27252 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))
290 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)))
291289, 290syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
292291rexlimdvva 3212 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
293219, 292biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
294218, 293jaod 858 . . . . 5 (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
295 reeanv 3227 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
29615adantr 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 𝑥)))))
29757adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 No )
29860ad2antrl 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 No )
29922a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s No )
30081ad2antrl 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
301300, 83syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
30273, 301eqeltrid 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
303296, 297, 298, 299, 302addsproplem1 27443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
304303simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No )
30595ad2antll 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
306103uneq2i 4160 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟))
307 naddword1 8687 . . . . . . . . . . . . . . . 16 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)))
308100, 68, 307mp2an 691 . . . . . . . . . . . . . . 15 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚))
309 ssequn2 4183 . . . . . . . . . . . . . . 15 (( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)) ↔ ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
310308, 309mpbi 229 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
311306, 310eqtri 2761 . . . . . . . . . . . . 13 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑚))
312 naddel1 8683 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚))))
313100, 39, 68, 312mp3an 1462 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
314114, 313sylib 217 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ( R ‘𝑋) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
315314ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
316 ontr1 6408 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) +no ( bday 𝑌)) ∈ On → (((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)) ∧ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
317206, 316ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)) ∧ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
318315, 300, 317syl2anc 585 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
319 elun1 4176 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) → (( bday 𝑟) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
320318, 319syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
321311, 320eqeltrid 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
322296, 305, 298, 299, 321addsproplem1 27443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑟) <s ( 0s +s 𝑟))))
323322simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No )
32420adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
325117ad2antll 728 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
326325, 119syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
327109, 326eqeltrid 2838 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
328296, 305, 324, 299, 327addsproplem1 27443 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
329328simpld 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No )
330 rightval 27349 . . . . . . . . . . . . . . . 16 ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟}
331330eleq2i 2826 . . . . . . . . . . . . . . 15 (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
332331biimpi 215 . . . . . . . . . . . . . 14 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
333332ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
334 rabid 3453 . . . . . . . . . . . . 13 (𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
335333, 334sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
336335simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
337 naddcom 8678 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
33868, 39, 337mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
339338, 300eqeltrid 2838 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
340 naddcom 8678 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
34168, 100, 340mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
342341, 318eqeltrid 2838 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
343 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) ∈ On)
34468, 39, 343mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) ∈ On
345 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) ∈ On)
34668, 100, 345mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) ∈ On
347 onunel 6467 . . . . . . . . . . . . . . . 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 𝑌)))))
348344, 346, 206, 347mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
349339, 342, 348sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
350 elun1 4176 . . . . . . . . . . . . . 14 (((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
351349, 350syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
352296, 298, 297, 305, 351addsproplem1 27443 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No ∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))))
353352simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))
354336, 353mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))
355 leftval 27348 . . . . . . . . . . . . . . . . 17 ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌}
356355eleq2i 2826 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
357356biimpi 215 . . . . . . . . . . . . . . 15 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
358357ad2antrl 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
359 rabid 3453 . . . . . . . . . . . . . 14 (𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
360358, 359sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
361360simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
362 naddcl 8673 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) +no ( bday 𝑚)) ∈ On)
363100, 68, 362mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑚)) ∈ On
364 naddcl 8673 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) +no ( bday 𝑌)) ∈ On)
365100, 31, 364mp2an 691 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑌)) ∈ On
366 onunel 6467 . . . . . . . . . . . . . . . . 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 𝑌)))))
367363, 365, 206, 366mp3an 1462 . . . . . . . . . . . . . . . 16 (((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
368318, 325, 367sylanbrc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
369 elun1 4176 . . . . . . . . . . . . . . 15 (((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
370368, 369syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
371296, 305, 298, 324, 370addsproplem1 27443 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))))
372371simprd 497 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))
373361, 372mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))
374305, 298addscomd 27441 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟))
375305, 324addscomd 27441 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟))
376373, 374, 3753brtr4d 5180 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌))
377304, 323, 329, 354, 376slttrd 27252 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))
378 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)))
379377, 378syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
380379rexlimdvva 3212 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
381295, 380biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
382 reeanv 3227 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
383 lltropt 27357 . . . . . . . . . . . . 13 ( L ‘𝑌) <<s ( R ‘𝑌)
384383a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
385 simprl 770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
386 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
387384, 385, 386ssltsepcd 27285 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠)
38815adantr 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 𝑥)))))
38957adantr 482 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
39060ad2antrl 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 No )
391131ad2antll 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
39281ad2antrl 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
393148ad2antll 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
394 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑋) +no ( bday 𝑚)) ∈ On)
39539, 68, 394mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑚)) ∈ On
396 naddcl 8673 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑋) +no ( bday 𝑠)) ∈ On)
39739, 135, 396mp2an 691 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑠)) ∈ On
398 onunel 6467 . . . . . . . . . . . . . . . 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 𝑌)))))
399395, 397, 206, 398mp3an 1462 . . . . . . . . . . . . . . 15 (((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) ↔ ((( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)) ∧ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
400392, 393, 399sylanbrc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
401 elun1 4176 . . . . . . . . . . . . . 14 (((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
402400, 401syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
403388, 389, 390, 391, 402addsproplem1 27443 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))))
404403simprd 497 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))
405387, 404mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))
406389, 390addscomd 27441 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋))
407389, 391addscomd 27441 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋))
408405, 406, 4073brtr4d 5180 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))
409 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)))
410408, 409syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
411410rexlimdvva 3212 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
412382, 411biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
413381, 412jaod 858 . . . . 5 (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
414294, 413jaod 858 . . . 4 (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏))
415182, 414biimtrid 241 . . 3 (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏))
4164153impib 1117 . 2 ((𝜑𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)
4177, 14, 92, 159, 416ssltd 27283 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 2710  wral 3062  wrex 3071  {crab 3433  Vcvv 3475  cun 3946  wss 3948  c0 4322   class class class wbr 5148  Oncon0 6362  cfv 6541  (class class class)co 7406   +no cnadd 8661   No csur 27133   <s cslt 27134   bday cbday 27135   <<s csslt 27272   0s c0s 27313   O cold 27328   L cleft 27330   R cright 27331   +s cadds 27433
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 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
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 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-1o 8463  df-2o 8464  df-nadd 8662  df-no 27136  df-slt 27137  df-bday 27138  df-sslt 27273  df-scut 27275  df-0s 27315  df-made 27332  df-old 27333  df-left 27335  df-right 27336  df-norec2 27423  df-adds 27434
This theorem is referenced by:  addsproplem3  27445
  Copyright terms: Public domain W3C validator