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

Theorem addsproplem2 28003
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 6919 . . . . 5 ( L ‘𝑋) ∈ V
21abrexex 7987 . . . 4 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V
32a1i 11 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V)
4 fvex 6919 . . . . 5 ( L ‘𝑌) ∈ V
54abrexex 7987 . . . 4 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V
65a1i 11 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V)
73, 6unexd 7774 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V)
8 fvex 6919 . . . . 5 ( R ‘𝑋) ∈ V
98abrexex 7987 . . . 4 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V
109a1i 11 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V)
11 fvex 6919 . . . . 5 ( R ‘𝑌) ∈ V
1211abrexex 7987 . . . 4 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V
1312a1i 11 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V)
1410, 13unexd 7774 . 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 480 . . . . . . . 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 27919 . . . . . . . . . 10 ( L ‘𝑋) ⊆ No
1817sseli 3979 . . . . . . . . 9 (𝑙 ∈ ( L ‘𝑋) → 𝑙 No )
1918adantl 481 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑙 No )
20 addsproplem2.3 . . . . . . . . 9 (𝜑𝑌 No )
2120adantr 480 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑌 No )
22 0sno 27871 . . . . . . . . 9 0s No
2322a1i 11 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 0s No )
24 bday0s 27873 . . . . . . . . . . . . 13 ( bday ‘ 0s ) = ∅
2524oveq2i 7442 . . . . . . . . . . . 12 (( bday 𝑙) +no ( bday ‘ 0s )) = (( bday 𝑙) +no ∅)
26 bdayelon 27821 . . . . . . . . . . . . 13 ( bday 𝑙) ∈ On
27 naddrid 8721 . . . . . . . . . . . . 13 (( bday 𝑙) ∈ On → (( bday 𝑙) +no ∅) = ( bday 𝑙))
2826, 27ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑙) +no ∅) = ( bday 𝑙)
2925, 28eqtri 2765 . . . . . . . . . . 11 (( bday 𝑙) +no ( bday ‘ 0s )) = ( bday 𝑙)
3029uneq2i 4165 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙))
31 bdayelon 27821 . . . . . . . . . . . 12 ( bday 𝑌) ∈ On
32 naddword1 8729 . . . . . . . . . . . 12 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)))
3326, 31, 32mp2an 692 . . . . . . . . . . 11 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌))
34 ssequn2 4189 . . . . . . . . . . 11 (( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)) ↔ ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌)))
3533, 34mpbi 230 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌))
3630, 35eqtri 2765 . . . . . . . . 9 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑌))
37 leftssold 27917 . . . . . . . . . . . . . 14 ( L ‘𝑋) ⊆ ( O ‘( bday 𝑋))
3837sseli 3979 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday 𝑋)))
39 bdayelon 27821 . . . . . . . . . . . . . 14 ( bday 𝑋) ∈ On
40 oldbday 27939 . . . . . . . . . . . . . 14 ((( bday 𝑋) ∈ On ∧ 𝑙 No ) → (𝑙 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑙) ∈ ( bday 𝑋)))
4139, 18, 40sylancr 587 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑙) ∈ ( bday 𝑋)))
4238, 41mpbid 232 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → ( bday 𝑙) ∈ ( bday 𝑋))
43 naddel1 8725 . . . . . . . . . . . . 13 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
4426, 39, 31, 43mp3an 1463 . . . . . . . . . . . 12 (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
4542, 44sylib 218 . . . . . . . . . . 11 (𝑙 ∈ ( L ‘𝑋) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
4645adantl 481 . . . . . . . . . 10 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
47 elun1 4182 . . . . . . . . . 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 2845 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
5016, 19, 21, 23, 49addsproplem1 28002 . . . . . . 7 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑙) <s ( 0s +s 𝑙))))
5150simpld 494 . . . . . 6 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No )
52 eleq1a 2836 . . . . . 6 ((𝑙 +s 𝑌) ∈ No → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5351, 52syl 17 . . . . 5 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5453rexlimdva 3155 . . . 4 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5554abssdv 4068 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ⊆ No )
5615adantr 480 . . . . . . . 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 480 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 𝑋 No )
59 leftssno 27919 . . . . . . . . . 10 ( L ‘𝑌) ⊆ No
6059sseli 3979 . . . . . . . . 9 (𝑚 ∈ ( L ‘𝑌) → 𝑚 No )
6160adantl 481 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 𝑚 No )
6222a1i 11 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → 0s No )
6324oveq2i 7442 . . . . . . . . . . . 12 (( bday 𝑋) +no ( bday ‘ 0s )) = (( bday 𝑋) +no ∅)
64 naddrid 8721 . . . . . . . . . . . . 13 (( bday 𝑋) ∈ On → (( bday 𝑋) +no ∅) = ( bday 𝑋))
6539, 64ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑋) +no ∅) = ( bday 𝑋)
6663, 65eqtri 2765 . . . . . . . . . . 11 (( bday 𝑋) +no ( bday ‘ 0s )) = ( bday 𝑋)
6766uneq2i 4165 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋))
68 bdayelon 27821 . . . . . . . . . . . 12 ( bday 𝑚) ∈ On
69 naddword1 8729 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)))
7039, 68, 69mp2an 692 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚))
71 ssequn2 4189 . . . . . . . . . . 11 (( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)) ↔ ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
7270, 71mpbi 230 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
7367, 72eqtri 2765 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑚))
74 leftssold 27917 . . . . . . . . . . . . . 14 ( L ‘𝑌) ⊆ ( O ‘( bday 𝑌))
7574sseli 3979 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday 𝑌)))
76 oldbday 27939 . . . . . . . . . . . . . 14 ((( bday 𝑌) ∈ On ∧ 𝑚 No ) → (𝑚 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑚) ∈ ( bday 𝑌)))
7731, 60, 76sylancr 587 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑚) ∈ ( bday 𝑌)))
7875, 77mpbid 232 . . . . . . . . . . . 12 (𝑚 ∈ ( L ‘𝑌) → ( bday 𝑚) ∈ ( bday 𝑌))
79 naddel2 8726 . . . . . . . . . . . . 13 ((( bday 𝑚) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
8068, 31, 39, 79mp3an 1463 . . . . . . . . . . . 12 (( bday 𝑚) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
8178, 80sylib 218 . . . . . . . . . . 11 (𝑚 ∈ ( L ‘𝑌) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
8281adantl 481 . . . . . . . . . 10 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
83 elun1 4182 . . . . . . . . . 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 2845 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8656, 58, 61, 62, 85addsproplem1 28002 . . . . . . 7 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
8786simpld 494 . . . . . 6 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No )
88 eleq1a 2836 . . . . . 6 ((𝑋 +s 𝑚) ∈ No → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
8987, 88syl 17 . . . . 5 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9089rexlimdva 3155 . . . 4 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9190abssdv 4068 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No )
9255, 91unssd 4192 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ⊆ No )
9315adantr 480 . . . . . . . 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 27920 . . . . . . . . . 10 ( R ‘𝑋) ⊆ No
9594sseli 3979 . . . . . . . . 9 (𝑟 ∈ ( R ‘𝑋) → 𝑟 No )
9695adantl 481 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑟 No )
9720adantr 480 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 𝑌 No )
9822a1i 11 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → 0s No )
9924oveq2i 7442 . . . . . . . . . . . 12 (( bday 𝑟) +no ( bday ‘ 0s )) = (( bday 𝑟) +no ∅)
100 bdayelon 27821 . . . . . . . . . . . . 13 ( bday 𝑟) ∈ On
101 naddrid 8721 . . . . . . . . . . . . 13 (( bday 𝑟) ∈ On → (( bday 𝑟) +no ∅) = ( bday 𝑟))
102100, 101ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑟) +no ∅) = ( bday 𝑟)
10399, 102eqtri 2765 . . . . . . . . . . 11 (( bday 𝑟) +no ( bday ‘ 0s )) = ( bday 𝑟)
104103uneq2i 4165 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟))
105 naddword1 8729 . . . . . . . . . . . 12 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)))
106100, 31, 105mp2an 692 . . . . . . . . . . 11 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌))
107 ssequn2 4189 . . . . . . . . . . 11 (( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)) ↔ ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌)))
108106, 107mpbi 230 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌))
109104, 108eqtri 2765 . . . . . . . . 9 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑌))
110 rightssold 27918 . . . . . . . . . . . . . 14 ( R ‘𝑋) ⊆ ( O ‘( bday 𝑋))
111110sseli 3979 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday 𝑋)))
112 oldbday 27939 . . . . . . . . . . . . . 14 ((( bday 𝑋) ∈ On ∧ 𝑟 No ) → (𝑟 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑟) ∈ ( bday 𝑋)))
11339, 95, 112sylancr 587 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘( bday 𝑋)) ↔ ( bday 𝑟) ∈ ( bday 𝑋)))
114111, 113mpbid 232 . . . . . . . . . . . 12 (𝑟 ∈ ( R ‘𝑋) → ( bday 𝑟) ∈ ( bday 𝑋))
115 naddel1 8725 . . . . . . . . . . . . 13 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
116100, 39, 31, 115mp3an 1463 . . . . . . . . . . . 12 (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
117114, 116sylib 218 . . . . . . . . . . 11 (𝑟 ∈ ( R ‘𝑋) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
118117adantl 481 . . . . . . . . . 10 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
119 elun1 4182 . . . . . . . . . 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 2845 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
12293, 96, 97, 98, 121addsproplem1 28002 . . . . . . 7 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
123122simpld 494 . . . . . 6 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No )
124 eleq1a 2836 . . . . . 6 ((𝑟 +s 𝑌) ∈ No → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
125123, 124syl 17 . . . . 5 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
126125rexlimdva 3155 . . . 4 (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
127126abssdv 4068 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ⊆ No )
12815adantr 480 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ∀𝑥 No 𝑦 No 𝑧 No (((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
12957adantr 480 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑋 No )
130 rightssno 27920 . . . . . . . . . 10 ( R ‘𝑌) ⊆ No
131130sseli 3979 . . . . . . . . 9 (𝑠 ∈ ( R ‘𝑌) → 𝑠 No )
132131adantl 481 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑠 No )
13322a1i 11 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 0s No )
13466uneq2i 4165 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋))
135 bdayelon 27821 . . . . . . . . . . . 12 ( bday 𝑠) ∈ On
136 naddword1 8729 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)))
13739, 135, 136mp2an 692 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠))
138 ssequn2 4189 . . . . . . . . . . 11 (( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)) ↔ ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
139137, 138mpbi 230 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
140134, 139eqtri 2765 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑠))
141 rightssold 27918 . . . . . . . . . . . . . 14 ( R ‘𝑌) ⊆ ( O ‘( bday 𝑌))
142141sseli 3979 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday 𝑌)))
143 oldbday 27939 . . . . . . . . . . . . . 14 ((( bday 𝑌) ∈ On ∧ 𝑠 No ) → (𝑠 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑠) ∈ ( bday 𝑌)))
14431, 131, 143sylancr 587 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘( bday 𝑌)) ↔ ( bday 𝑠) ∈ ( bday 𝑌)))
145142, 144mpbid 232 . . . . . . . . . . . 12 (𝑠 ∈ ( R ‘𝑌) → ( bday 𝑠) ∈ ( bday 𝑌))
146 naddel2 8726 . . . . . . . . . . . . 13 ((( bday 𝑠) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
147135, 31, 39, 146mp3an 1463 . . . . . . . . . . . 12 (( bday 𝑠) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
148145, 147sylib 218 . . . . . . . . . . 11 (𝑠 ∈ ( R ‘𝑌) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
149148adantl 481 . . . . . . . . . 10 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
150 elun1 4182 . . . . . . . . . 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 2845 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
153128, 129, 132, 133, 152addsproplem1 28002 . . . . . . 7 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑋) <s ( 0s +s 𝑋))))
154153simpld 494 . . . . . 6 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No )
155 eleq1a 2836 . . . . . 6 ((𝑋 +s 𝑠) ∈ No → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
156154, 155syl 17 . . . . 5 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
157156rexlimdva 3155 . . . 4 (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
158157abssdv 4068 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No )
159127, 158unssd 4192 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No )
160 elun 4153 . . . . . . 7 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}))
161 vex 3484 . . . . . . . . 9 𝑎 ∈ V
162 eqeq1 2741 . . . . . . . . . 10 (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌)))
163162rexbidv 3179 . . . . . . . . 9 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)))
164161, 163elab 3679 . . . . . . . 8 (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))
165 eqeq1 2741 . . . . . . . . . 10 (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚)))
166165rexbidv 3179 . . . . . . . . 9 (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
167161, 166elab 3679 . . . . . . . 8 (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))
168164, 167orbi12i 915 . . . . . . 7 ((𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
169160, 168bitri 275 . . . . . 6 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
170 elun 4153 . . . . . . 7 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
171 vex 3484 . . . . . . . . 9 𝑏 ∈ V
172 eqeq1 2741 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌)))
173172rexbidv 3179 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
174171, 173elab 3679 . . . . . . . 8 (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))
175 eqeq1 2741 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠)))
176175rexbidv 3179 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
177171, 176elab 3679 . . . . . . . 8 (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))
178174, 177orbi12i 915 . . . . . . 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 1013 . . . . 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 3229 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
184 lltropt 27911 . . . . . . . . . . . 12 ( L ‘𝑋) <<s ( R ‘𝑋)
185184a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
186 simprl 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
187 simprr 773 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
188185, 186, 187ssltsepcd 27839 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟)
18915adantr 480 . . . . . . . . . . . 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 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
19118ad2antrl 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 No )
19295ad2antll 729 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
193 naddcom 8720 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌)))
19431, 26, 193mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑌))
19545ad2antrl 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
196194, 195eqeltrid 2845 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
197 naddcom 8720 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌)))
19831, 100, 197mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑌))
199117ad2antll 729 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
200198, 199eqeltrid 2845 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
201 naddcl 8715 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) ∈ On)
20231, 26, 201mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) ∈ On
203 naddcl 8715 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) ∈ On)
20431, 100, 203mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) ∈ On
205 naddcl 8715 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑋) +no ( bday 𝑌)) ∈ On)
20639, 31, 205mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑋) +no ( bday 𝑌)) ∈ On
207 onunel 6489 . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑌) +no ( bday 𝑙)) ∪ (( bday 𝑌) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
210 elun1 4182 . . . . . . . . . . . . 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 28002 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))))
213212simprd 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
214188, 213mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))
215 breq12 5148 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
216214, 215syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
217216rexlimdvva 3213 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
218183, 217biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
219 reeanv 3229 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
22051adantrr 717 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No )
22115adantr 480 . . . . . . . . . . . 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 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 No )
223131ad2antll 729 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
22422a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s No )
22529uneq2i 4165 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙))
226 naddword1 8729 . . . . . . . . . . . . . . . 16 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)))
22726, 135, 226mp2an 692 . . . . . . . . . . . . . . 15 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠))
228 ssequn2 4189 . . . . . . . . . . . . . . 15 (( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)) ↔ ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
229227, 228mpbi 230 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
230225, 229eqtri 2765 . . . . . . . . . . . . 13 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑠))
231 naddel1 8725 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠))))
23226, 39, 135, 231mp3an 1463 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
23342, 232sylib 218 . . . . . . . . . . . . . . . 16 (𝑙 ∈ ( L ‘𝑋) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
234233ad2antrl 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠)))
235148ad2antll 729 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
236 ontr1 6430 . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
239 elun1 4182 . . . . . . . . . . . . . 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 2845 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
242221, 222, 223, 224, 241addsproplem1 28002 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑙) <s ( 0s +s 𝑙))))
243242simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No )
244154adantrl 716 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No )
245 rightval 27903 . . . . . . . . . . . . . . 15 ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday 𝑌)) ∣ 𝑌 <s 𝑠}
246245reqabi 3460 . . . . . . . . . . . . . 14 (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘( bday 𝑌)) ∧ 𝑌 <s 𝑠))
247246simprbi 496 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
248247ad2antll 729 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
24920adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 No )
25045ad2antrl 728 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
251 naddcl 8715 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) +no ( bday 𝑌)) ∈ On)
25226, 31, 251mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑌)) ∈ On
253 naddcl 8715 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) +no ( bday 𝑠)) ∈ On)
25426, 135, 253mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑠)) ∈ On
255 onunel 6489 . . . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
258 elun1 4182 . . . . . . . . . . . . . . 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 28002 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))))
261260simprd 495 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))
262248, 261mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))
263222, 249addscomd 28000 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙))
264222, 223addscomd 28000 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙))
265262, 263, 2643brtr4d 5175 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠))
266 leftval 27902 . . . . . . . . . . . . . 14 ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday 𝑋)) ∣ 𝑙 <s 𝑋}
267266reqabi 3460 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday 𝑋)) ∧ 𝑙 <s 𝑋))
268267simprbi 496 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
269268ad2antrl 728 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
27057adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
271 naddcom 8720 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
272135, 26, 271mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
273272, 238eqeltrid 2845 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
274 naddcom 8720 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
275135, 39, 274mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
276275, 235eqeltrid 2845 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
277 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) ∈ On)
278135, 26, 277mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) ∈ On
279 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) ∈ On)
280135, 39, 279mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) ∈ On
281 onunel 6489 . . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑠) +no ( bday 𝑙)) ∪ (( bday 𝑠) +no ( bday 𝑋))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
284 elun1 4182 . . . . . . . . . . . . . 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 28002 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))))
287286simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))
288269, 287mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))
289220, 243, 244, 265, 288slttrd 27804 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))
290 breq12 5148 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)))
291289, 290syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
292291rexlimdvva 3213 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
293219, 292biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
294218, 293jaod 860 . . . . 5 (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
295 reeanv 3229 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
29615adantr 480 . . . . . . . . . . . 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 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 No )
29860ad2antrl 728 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 No )
29922a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s No )
30081ad2antrl 728 . . . . . . . . . . . . . 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 2845 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
303296, 297, 298, 299, 302addsproplem1 28002 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
304303simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No )
30595ad2antll 729 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 No )
306103uneq2i 4165 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟))
307 naddword1 8729 . . . . . . . . . . . . . . . 16 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)))
308100, 68, 307mp2an 692 . . . . . . . . . . . . . . 15 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚))
309 ssequn2 4189 . . . . . . . . . . . . . . 15 (( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)) ↔ ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
310308, 309mpbi 230 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
311306, 310eqtri 2765 . . . . . . . . . . . . 13 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑚))
312 naddel1 8725 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚))))
313100, 39, 68, 312mp3an 1463 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
314114, 313sylib 218 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ( R ‘𝑋) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
315314ad2antll 729 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚)))
316 ontr1 6430 . . . . . . . . . . . . . . . 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 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
319 elun1 4182 . . . . . . . . . . . . . 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 2845 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
322296, 305, 298, 299, 321addsproplem1 28002 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑟) <s ( 0s +s 𝑟))))
323322simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No )
32420adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 No )
325117ad2antll 729 . . . . . . . . . . . . . 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 2845 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
328296, 305, 324, 299, 327addsproplem1 28002 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
329328simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No )
330 rightval 27903 . . . . . . . . . . . . . . . 16 ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟}
331330eleq2i 2833 . . . . . . . . . . . . . . 15 (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
332331biimpi 216 . . . . . . . . . . . . . 14 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
333332ad2antll 729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
334 rabid 3458 . . . . . . . . . . . . 13 (𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
335333, 334sylib 218 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
336335simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
337 naddcom 8720 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
33868, 39, 337mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
339338, 300eqeltrid 2845 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
340 naddcom 8720 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
34168, 100, 340mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
342341, 318eqeltrid 2845 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
343 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) ∈ On)
34468, 39, 343mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) ∈ On
345 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) ∈ On)
34668, 100, 345mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) ∈ On
347 onunel 6489 . . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑚) +no ( bday 𝑋)) ∪ (( bday 𝑚) +no ( bday 𝑟))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
350 elun1 4182 . . . . . . . . . . . . . 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 28002 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No ∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))))
353352simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))
354336, 353mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))
355 leftval 27902 . . . . . . . . . . . . . . . . 17 ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌}
356355eleq2i 2833 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
357356biimpi 216 . . . . . . . . . . . . . . 15 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
358357ad2antrl 728 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
359 rabid 3458 . . . . . . . . . . . . . 14 (𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
360358, 359sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
361360simprd 495 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
362 naddcl 8715 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) +no ( bday 𝑚)) ∈ On)
363100, 68, 362mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑚)) ∈ On
364 naddcl 8715 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) +no ( bday 𝑌)) ∈ On)
365100, 31, 364mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑌)) ∈ On
366 onunel 6489 . . . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday 𝑌))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
369 elun1 4182 . . . . . . . . . . . . . . 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 28002 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))))
372371simprd 495 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))
373361, 372mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))
374305, 298addscomd 28000 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟))
375305, 324addscomd 28000 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟))
376373, 374, 3753brtr4d 5175 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌))
377304, 323, 329, 354, 376slttrd 27804 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))
378 breq12 5148 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)))
379377, 378syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
380379rexlimdvva 3213 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
381295, 380biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
382 reeanv 3229 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
383 lltropt 27911 . . . . . . . . . . . . 13 ( L ‘𝑌) <<s ( R ‘𝑌)
384383a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
385 simprl 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
386 simprr 773 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
387384, 385, 386ssltsepcd 27839 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠)
38815adantr 480 . . . . . . . . . . . . 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 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
39060ad2antrl 728 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 No )
391131ad2antll 729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 No )
39281ad2antrl 728 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
393148ad2antll 729 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
394 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑋) +no ( bday 𝑚)) ∈ On)
39539, 68, 394mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑚)) ∈ On
396 naddcl 8715 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑋) +no ( bday 𝑠)) ∈ On)
39739, 135, 396mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑠)) ∈ On
398 onunel 6489 . . . . . . . . . . . . . . . 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 1463 . . . . . . . . . . . . . . 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 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday 𝑠))) ∈ (( bday 𝑋) +no ( bday 𝑌)))
401 elun1 4182 . . . . . . . . . . . . . 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 28002 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))))
404403simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))
405387, 404mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))
406389, 390addscomd 28000 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋))
407389, 391addscomd 28000 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋))
408405, 406, 4073brtr4d 5175 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))
409 breq12 5148 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)))
410408, 409syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
411410rexlimdvva 3213 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
412382, 411biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
413381, 412jaod 860 . . . . 5 (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
414294, 413jaod 860 . . . 4 (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏))
415182, 414biimtrid 242 . . 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 27836 1 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cun 3949  wss 3951  c0 4333   class class class wbr 5143  Oncon0 6384  cfv 6561  (class class class)co 7431   +no cnadd 8703   No csur 27684   <s cslt 27685   bday cbday 27686   <<s csslt 27825   0s c0s 27867   O cold 27882   L cleft 27884   R cright 27885   +s cadds 27992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-1o 8506  df-2o 8507  df-nadd 8704  df-no 27687  df-slt 27688  df-bday 27689  df-sslt 27826  df-scut 27828  df-0s 27869  df-made 27886  df-old 27887  df-left 27889  df-right 27890  df-norec2 27982  df-adds 27993
This theorem is referenced by:  addsproplem3  28004
  Copyright terms: Public domain W3C validator