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

Theorem addsproplem2 28018
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 6920 . . . . 5 ( L ‘𝑋) ∈ V
21abrexex 7986 . . . 4 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V
32a1i 11 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V)
4 fvex 6920 . . . . 5 ( L ‘𝑌) ∈ V
54abrexex 7986 . . . 4 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V
65a1i 11 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V)
73, 6unexd 7773 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V)
8 fvex 6920 . . . . 5 ( R ‘𝑋) ∈ V
98abrexex 7986 . . . 4 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V
109a1i 11 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V)
11 fvex 6920 . . . . 5 ( R ‘𝑌) ∈ V
1211abrexex 7986 . . . 4 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V
1312a1i 11 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V)
1410, 13unexd 7773 . 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 27934 . . . . . . . . . 10 ( L ‘𝑋) ⊆ No
1817sseli 3991 . . . . . . . . 9 (𝑙 ∈ ( L ‘𝑋) → 𝑙 No )
1918adantl 481 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑙 No )
20 addsproplem2.3 . . . . . . . . 9 (𝜑𝑌 No )
2120adantr 480 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 𝑌 No )
22 0sno 27886 . . . . . . . . 9 0s No
2322a1i 11 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → 0s No )
24 bday0s 27888 . . . . . . . . . . . . 13 ( bday ‘ 0s ) = ∅
2524oveq2i 7442 . . . . . . . . . . . 12 (( bday 𝑙) +no ( bday ‘ 0s )) = (( bday 𝑙) +no ∅)
26 bdayelon 27836 . . . . . . . . . . . . 13 ( bday 𝑙) ∈ On
27 naddrid 8720 . . . . . . . . . . . . 13 (( bday 𝑙) ∈ On → (( bday 𝑙) +no ∅) = ( bday 𝑙))
2826, 27ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑙) +no ∅) = ( bday 𝑙)
2925, 28eqtri 2763 . . . . . . . . . . 11 (( bday 𝑙) +no ( bday ‘ 0s )) = ( bday 𝑙)
3029uneq2i 4175 . . . . . . . . . 10 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑌)) ∪ ( bday 𝑙))
31 bdayelon 27836 . . . . . . . . . . . 12 ( bday 𝑌) ∈ On
32 naddword1 8728 . . . . . . . . . . . 12 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌)))
3326, 31, 32mp2an 692 . . . . . . . . . . 11 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑌))
34 ssequn2 4199 . . . . . . . . . . 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 2763 . . . . . . . . 9 ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑌))
37 leftssold 27932 . . . . . . . . . . . . . 14 ( L ‘𝑋) ⊆ ( O ‘( bday 𝑋))
3837sseli 3991 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday 𝑋)))
39 bdayelon 27836 . . . . . . . . . . . . . 14 ( bday 𝑋) ∈ On
40 oldbday 27954 . . . . . . . . . . . . . 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 8724 . . . . . . . . . . . . 13 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
4426, 39, 31, 43mp3an 1460 . . . . . . . . . . . 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 4192 . . . . . . . . . 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 2843 . . . . . . . 8 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((( bday 𝑙) +no ( bday 𝑌)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
5016, 19, 21, 23, 49addsproplem1 28017 . . . . . . 7 ((𝜑𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑙) <s ( 0s +s 𝑙))))
5150simpld 494 . . . . . 6 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No )
52 eleq1a 2834 . . . . . 6 ((𝑙 +s 𝑌) ∈ No → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5351, 52syl 17 . . . . 5 ((𝜑𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5453rexlimdva 3153 . . . 4 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 No ))
5554abssdv 4078 . . 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 27934 . . . . . . . . . 10 ( L ‘𝑌) ⊆ No
6059sseli 3991 . . . . . . . . 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 8720 . . . . . . . . . . . . 13 (( bday 𝑋) ∈ On → (( bday 𝑋) +no ∅) = ( bday 𝑋))
6539, 64ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑋) +no ∅) = ( bday 𝑋)
6663, 65eqtri 2763 . . . . . . . . . . 11 (( bday 𝑋) +no ( bday ‘ 0s )) = ( bday 𝑋)
6766uneq2i 4175 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑚)) ∪ ( bday 𝑋))
68 bdayelon 27836 . . . . . . . . . . . 12 ( bday 𝑚) ∈ On
69 naddword1 8728 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚)))
7039, 68, 69mp2an 692 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑚))
71 ssequn2 4199 . . . . . . . . . . 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 2763 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑚))
74 leftssold 27932 . . . . . . . . . . . . . 14 ( L ‘𝑌) ⊆ ( O ‘( bday 𝑌))
7574sseli 3991 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday 𝑌)))
76 oldbday 27954 . . . . . . . . . . . . . 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 8725 . . . . . . . . . . . . 13 ((( bday 𝑚) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
8068, 31, 39, 79mp3an 1460 . . . . . . . . . . . 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 4192 . . . . . . . . . 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 2843 . . . . . . . 8 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
8656, 58, 61, 62, 85addsproplem1 28017 . . . . . . 7 ((𝜑𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
8786simpld 494 . . . . . 6 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No )
88 eleq1a 2834 . . . . . 6 ((𝑋 +s 𝑚) ∈ No → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
8987, 88syl 17 . . . . 5 ((𝜑𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9089rexlimdva 3153 . . . 4 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 No ))
9190abssdv 4078 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No )
9255, 91unssd 4202 . 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 27935 . . . . . . . . . 10 ( R ‘𝑋) ⊆ No
9594sseli 3991 . . . . . . . . 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 27836 . . . . . . . . . . . . 13 ( bday 𝑟) ∈ On
101 naddrid 8720 . . . . . . . . . . . . 13 (( bday 𝑟) ∈ On → (( bday 𝑟) +no ∅) = ( bday 𝑟))
102100, 101ax-mp 5 . . . . . . . . . . . 12 (( bday 𝑟) +no ∅) = ( bday 𝑟)
10399, 102eqtri 2763 . . . . . . . . . . 11 (( bday 𝑟) +no ( bday ‘ 0s )) = ( bday 𝑟)
104103uneq2i 4175 . . . . . . . . . 10 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑌)) ∪ ( bday 𝑟))
105 naddword1 8728 . . . . . . . . . . . 12 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌)))
106100, 31, 105mp2an 692 . . . . . . . . . . 11 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑌))
107 ssequn2 4199 . . . . . . . . . . 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 2763 . . . . . . . . 9 ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑌))
110 rightssold 27933 . . . . . . . . . . . . . 14 ( R ‘𝑋) ⊆ ( O ‘( bday 𝑋))
111110sseli 3991 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday 𝑋)))
112 oldbday 27954 . . . . . . . . . . . . . 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 8724 . . . . . . . . . . . . 13 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑌)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
116100, 39, 31, 115mp3an 1460 . . . . . . . . . . . 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 4192 . . . . . . . . . 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 2843 . . . . . . . 8 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
12293, 96, 97, 98, 121addsproplem1 28017 . . . . . . 7 ((𝜑𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
123122simpld 494 . . . . . 6 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No )
124 eleq1a 2834 . . . . . 6 ((𝑟 +s 𝑌) ∈ No → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
125123, 124syl 17 . . . . 5 ((𝜑𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
126125rexlimdva 3153 . . . 4 (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 No ))
127126abssdv 4078 . . 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 27935 . . . . . . . . . 10 ( R ‘𝑌) ⊆ No
131130sseli 3991 . . . . . . . . 9 (𝑠 ∈ ( R ‘𝑌) → 𝑠 No )
132131adantl 481 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 𝑠 No )
13322a1i 11 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → 0s No )
13466uneq2i 4175 . . . . . . . . . 10 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = ((( bday 𝑋) +no ( bday 𝑠)) ∪ ( bday 𝑋))
135 bdayelon 27836 . . . . . . . . . . . 12 ( bday 𝑠) ∈ On
136 naddword1 8728 . . . . . . . . . . . 12 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠)))
13739, 135, 136mp2an 692 . . . . . . . . . . 11 ( bday 𝑋) ⊆ (( bday 𝑋) +no ( bday 𝑠))
138 ssequn2 4199 . . . . . . . . . . 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 2763 . . . . . . . . 9 ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) = (( bday 𝑋) +no ( bday 𝑠))
141 rightssold 27933 . . . . . . . . . . . . . 14 ( R ‘𝑌) ⊆ ( O ‘( bday 𝑌))
142141sseli 3991 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday 𝑌)))
143 oldbday 27954 . . . . . . . . . . . . . 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 8725 . . . . . . . . . . . . 13 ((( bday 𝑠) ∈ On ∧ ( bday 𝑌) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) ∈ ( bday 𝑌) ↔ (( bday 𝑋) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑌))))
147135, 31, 39, 146mp3an 1460 . . . . . . . . . . . 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 4192 . . . . . . . . . 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 2843 . . . . . . . 8 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((( bday 𝑋) +no ( bday 𝑠)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
153128, 129, 132, 133, 152addsproplem1 28017 . . . . . . 7 ((𝜑𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑋) <s ( 0s +s 𝑋))))
154153simpld 494 . . . . . 6 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No )
155 eleq1a 2834 . . . . . 6 ((𝑋 +s 𝑠) ∈ No → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
156154, 155syl 17 . . . . 5 ((𝜑𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
157156rexlimdva 3153 . . . 4 (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 No ))
158157abssdv 4078 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No )
159127, 158unssd 4202 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No )
160 elun 4163 . . . . . . 7 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}))
161 vex 3482 . . . . . . . . 9 𝑎 ∈ V
162 eqeq1 2739 . . . . . . . . . 10 (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌)))
163162rexbidv 3177 . . . . . . . . 9 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)))
164161, 163elab 3681 . . . . . . . 8 (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))
165 eqeq1 2739 . . . . . . . . . 10 (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚)))
166165rexbidv 3177 . . . . . . . . 9 (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
167161, 166elab 3681 . . . . . . . 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 4163 . . . . . . 7 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
171 vex 3482 . . . . . . . . 9 𝑏 ∈ V
172 eqeq1 2739 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌)))
173172rexbidv 3177 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
174171, 173elab 3681 . . . . . . . 8 (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))
175 eqeq1 2739 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠)))
176175rexbidv 3177 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
177171, 176elab 3681 . . . . . . . 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 1012 . . . . 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 27926 . . . . . . . . . . . 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 27854 . . . . . . . . . 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 8719 . . . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
197 naddcom 8719 . . . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑌) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
201 naddcl 8714 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑌) +no ( bday 𝑙)) ∈ On)
20231, 26, 201mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑙)) ∈ On
203 naddcl 8714 . . . . . . . . . . . . . . . 16 ((( bday 𝑌) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑌) +no ( bday 𝑟)) ∈ On)
20431, 100, 203mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑌) +no ( bday 𝑟)) ∈ On
205 naddcl 8714 . . . . . . . . . . . . . . . 16 ((( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑋) +no ( bday 𝑌)) ∈ On)
20639, 31, 205mp2an 692 . . . . . . . . . . . . . . 15 (( bday 𝑋) +no ( bday 𝑌)) ∈ On
207 onunel 6491 . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . 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 28017 . . . . . . . . . . 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 5153 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
216214, 215syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
217216rexlimdvva 3211 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
218183, 217biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
219 reeanv 3227 . . . . . . 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 4175 . . . . . . . . . . . . . 14 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = ((( bday 𝑙) +no ( bday 𝑠)) ∪ ( bday 𝑙))
226 naddword1 8728 . . . . . . . . . . . . . . . 16 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠)))
22726, 135, 226mp2an 692 . . . . . . . . . . . . . . 15 ( bday 𝑙) ⊆ (( bday 𝑙) +no ( bday 𝑠))
228 ssequn2 4199 . . . . . . . . . . . . . . 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 2763 . . . . . . . . . . . . 13 ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) = (( bday 𝑙) +no ( bday 𝑠))
231 naddel1 8724 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) ∈ ( bday 𝑋) ↔ (( bday 𝑙) +no ( bday 𝑠)) ∈ (( bday 𝑋) +no ( bday 𝑠))))
23226, 39, 135, 231mp3an 1460 . . . . . . . . . . . . . . . . 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 6432 . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday 𝑙) +no ( bday 𝑠)) ∪ (( bday 𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
242221, 222, 223, 224, 241addsproplem1 28017 . . . . . . . . . . 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 27918 . . . . . . . . . . . . . . 15 ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday 𝑌)) ∣ 𝑌 <s 𝑠}
246245reqabi 3457 . . . . . . . . . . . . . 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 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑙) +no ( bday 𝑌)) ∈ On)
25226, 31, 251mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑌)) ∈ On
253 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑙) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑙) +no ( bday 𝑠)) ∈ On)
25426, 135, 253mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑙) +no ( bday 𝑠)) ∈ On
255 onunel 6491 . . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . . 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 28017 . . . . . . . . . . . . 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 28015 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙))
264222, 223addscomd 28015 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙))
265262, 263, 2643brtr4d 5180 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠))
266 leftval 27917 . . . . . . . . . . . . . 14 ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday 𝑋)) ∣ 𝑙 <s 𝑋}
267266reqabi 3457 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday 𝑋)) ∧ 𝑙 <s 𝑋))
268267simprbi 496 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
269268ad2antrl 728 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
27057adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 No )
271 naddcom 8719 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠)))
272135, 26, 271mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) = (( bday 𝑙) +no ( bday 𝑠))
273272, 238eqeltrid 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑙)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
274 naddcom 8719 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠)))
275135, 39, 274mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑠))
276275, 235eqeltrid 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday 𝑠) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
277 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑙) ∈ On) → (( bday 𝑠) +no ( bday 𝑙)) ∈ On)
278135, 26, 277mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑙)) ∈ On
279 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑠) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑠) +no ( bday 𝑋)) ∈ On)
280135, 39, 279mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑠) +no ( bday 𝑋)) ∈ On
281 onunel 6491 . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 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 28017 . . . . . . . . . . . 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 27819 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))
290 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)))
291289, 290syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
292291rexlimdvva 3211 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
293219, 292biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
294218, 293jaod 859 . . . . 5 (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
295 reeanv 3227 . . . . . . 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 2843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑋) +no ( bday 𝑚)) ∪ (( bday 𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
303296, 297, 298, 299, 302addsproplem1 28017 . . . . . . . . . . 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 4175 . . . . . . . . . . . . . 14 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = ((( bday 𝑟) +no ( bday 𝑚)) ∪ ( bday 𝑟))
307 naddword1 8728 . . . . . . . . . . . . . . . 16 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚)))
308100, 68, 307mp2an 692 . . . . . . . . . . . . . . 15 ( bday 𝑟) ⊆ (( bday 𝑟) +no ( bday 𝑚))
309 ssequn2 4199 . . . . . . . . . . . . . . 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 2763 . . . . . . . . . . . . 13 ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) = (( bday 𝑟) +no ( bday 𝑚))
312 naddel1 8724 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) ∈ ( bday 𝑋) ↔ (( bday 𝑟) +no ( bday 𝑚)) ∈ (( bday 𝑋) +no ( bday 𝑚))))
313100, 39, 68, 312mp3an 1460 . . . . . . . . . . . . . . . . 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 6432 . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑚)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
322296, 305, 298, 299, 321addsproplem1 28017 . . . . . . . . . . 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 2843 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday 𝑟) +no ( bday 𝑌)) ∪ (( bday 𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
328296, 305, 324, 299, 327addsproplem1 28017 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
329328simpld 494 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No )
330 rightval 27918 . . . . . . . . . . . . . . . 16 ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟}
331330eleq2i 2831 . . . . . . . . . . . . . . 15 (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
332331biimpi 216 . . . . . . . . . . . . . 14 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
333332ad2antll 729 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟})
334 rabid 3455 . . . . . . . . . . . . 13 (𝑟 ∈ {𝑟 ∈ ( O ‘( bday 𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
335333, 334sylib 218 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday 𝑋)) ∧ 𝑋 <s 𝑟))
336335simprd 495 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
337 naddcom 8719 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚)))
33868, 39, 337mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) = (( bday 𝑋) +no ( bday 𝑚))
339338, 300eqeltrid 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑋)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
340 naddcom 8719 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚)))
34168, 100, 340mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) = (( bday 𝑟) +no ( bday 𝑚))
342341, 318eqeltrid 2843 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday 𝑚) +no ( bday 𝑟)) ∈ (( bday 𝑋) +no ( bday 𝑌)))
343 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑋) ∈ On) → (( bday 𝑚) +no ( bday 𝑋)) ∈ On)
34468, 39, 343mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑋)) ∈ On
345 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑚) ∈ On ∧ ( bday 𝑟) ∈ On) → (( bday 𝑚) +no ( bday 𝑟)) ∈ On)
34668, 100, 345mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑚) +no ( bday 𝑟)) ∈ On
347 onunel 6491 . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 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 28017 . . . . . . . . . . . 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 27917 . . . . . . . . . . . . . . . . 17 ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌}
356355eleq2i 2831 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
357356biimpi 216 . . . . . . . . . . . . . . 15 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
358357ad2antrl 728 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌})
359 rabid 3455 . . . . . . . . . . . . . 14 (𝑚 ∈ {𝑚 ∈ ( O ‘( bday 𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
360358, 359sylib 218 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday 𝑌)) ∧ 𝑚 <s 𝑌))
361360simprd 495 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
362 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑟) +no ( bday 𝑚)) ∈ On)
363100, 68, 362mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑚)) ∈ On
364 naddcl 8714 . . . . . . . . . . . . . . . . . 18 ((( bday 𝑟) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑟) +no ( bday 𝑌)) ∈ On)
365100, 31, 364mp2an 692 . . . . . . . . . . . . . . . . 17 (( bday 𝑟) +no ( bday 𝑌)) ∈ On
366 onunel 6491 . . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . . 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 28017 . . . . . . . . . . . . 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 28015 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟))
375305, 324addscomd 28015 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟))
376373, 374, 3753brtr4d 5180 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌))
377304, 323, 329, 354, 376slttrd 27819 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))
378 breq12 5153 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)))
379377, 378syl5ibrcom 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
380379rexlimdvva 3211 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
381295, 380biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
382 reeanv 3227 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
383 lltropt 27926 . . . . . . . . . . . . 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 27854 . . . . . . . . . . 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 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑚) ∈ On) → (( bday 𝑋) +no ( bday 𝑚)) ∈ On)
39539, 68, 394mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑚)) ∈ On
396 naddcl 8714 . . . . . . . . . . . . . . . . 17 ((( bday 𝑋) ∈ On ∧ ( bday 𝑠) ∈ On) → (( bday 𝑋) +no ( bday 𝑠)) ∈ On)
39739, 135, 396mp2an 692 . . . . . . . . . . . . . . . 16 (( bday 𝑋) +no ( bday 𝑠)) ∈ On
398 onunel 6491 . . . . . . . . . . . . . . . 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 1460 . . . . . . . . . . . . . . 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 4192 . . . . . . . . . . . . . 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 28017 . . . . . . . . . . . 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 28015 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋))
407389, 391addscomd 28015 . . . . . . . . . 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 247 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
411410rexlimdvva 3211 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
412382, 411biimtrrid 243 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
413381, 412jaod 859 . . . . 5 (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
414294, 413jaod 859 . . . 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 1115 . 2 ((𝜑𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)
4177, 14, 92, 159, 416ssltd 27851 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 847   = wceq 1537  wcel 2106  {cab 2712  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  cun 3961  wss 3963  c0 4339   class class class wbr 5148  Oncon0 6386  cfv 6563  (class class class)co 7431   +no cnadd 8702   No csur 27699   <s cslt 27700   bday cbday 27701   <<s csslt 27840   0s c0s 27882   O cold 27897   L cleft 27899   R cright 27900   +s cadds 28007
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-1o 8505  df-2o 8506  df-nadd 8703  df-no 27702  df-slt 27703  df-bday 27704  df-sslt 27841  df-scut 27843  df-0s 27884  df-made 27901  df-old 27902  df-left 27904  df-right 27905  df-norec2 27997  df-adds 28008
This theorem is referenced by:  addsproplem3  28019
  Copyright terms: Public domain W3C validator