Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  addsproplem2 Structured version   Visualization version   GIF version
Theorem addsproplem2 34308
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 6853 . . . . 5 ( L ‘𝑋) ∈ V
21abrexex 7892 . . . 4 {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V
32a1i 11 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V)
4 fvex 6853 . . . . 5 ( L ‘𝑌) ∈ V
54abrexex 7892 . . . 4 {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V
65a1i 11 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V)
73, 6unexd 7685 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V)
8 fvex 6853 . . . . 5 ( R ‘𝑋) ∈ V
98abrexex 7892 . . . 4 {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V
109a1i 11 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V)
11 fvex 6853 . . . . 5 ( R ‘𝑌) ∈ V
1211abrexex 7892 . . . 4 {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V
1312a1i 11 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V)
1410, 13unexd 7685 . 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 481 . . . . . . . 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 27206 . . . . . . . . . 10 ( L ‘𝑋) ⊆ No
1817sseli 3939 . . . . . . . . 9 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ No )
1918adantl 482 . . . . . . . 8 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑙 ∈ No )
20 addsproplem2.3 . . . . . . . . 9 (𝜑 → 𝑌 ∈ No )
2120adantr 481 . . . . . . . 8 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑌 ∈ No )
22 0sno 27161 . . . . . . . . 9 0s ∈ No
2322a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 0s ∈ No )
24 bday0s 27163 . . . . . . . . . . . . 13 ( bday ‘ 0s ) = ∅
2524oveq2i 7365 . . . . . . . . . . . 12 (( bday ‘𝑙) +no ( bday ‘ 0s )) = (( bday ‘𝑙) +no ∅)
26 bdayelon 27112 . . . . . . . . . . . . 13 ( bday ‘𝑙) ∈ On
27 naddid1 8626 . . . . . . . . . . . . 13 (( bday ‘𝑙) ∈ On → (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙))
2826, 27ax-mp 5 . . . . . . . . . . . 12 (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙)
2925, 28eqtri 2764 . . . . . . . . . . 11 (( bday ‘𝑙) +no ( bday ‘ 0s )) = ( bday ‘𝑙)
3029uneq2i 4119 . . . . . . . . . 10 ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙))
31 bdayelon 27112 . . . . . . . . . . . 12 ( bday ‘𝑌) ∈ On
32 naddword1 8633 . . . . . . . . . . . 12 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌)))
3326, 31, 32mp2an 690 . . . . . . . . . . 11 ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌))
34 ssequn2 4142 . . . . . . . . . . 11 (( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌)))
3533, 34mpbi 229 . . . . . . . . . 10 ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌))
3630, 35eqtri 2764 . . . . . . . . 9 ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) = (( bday ‘𝑙) +no ( bday ‘𝑌))
37 leftssold 27204 . . . . . . . . . . . . . 14 ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
3837sseli 3939 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday ‘𝑋)))
39 bdayelon 27112 . . . . . . . . . . . . . 14 ( bday ‘𝑋) ∈ On
40 oldbday 27226 . . . . . . . . . . . . . 14 ((( bday ‘𝑋) ∈ On ∧ 𝑙 ∈ No ) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
4139, 18, 40sylancr 587 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
4238, 41mpbid 231 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → ( bday ‘𝑙) ∈ ( bday ‘𝑋))
43 naddel1 8629 . . . . . . . . . . . . 13 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
4426, 39, 31, 43mp3an 1461 . . . . . . . . . . . 12 (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
4542, 44sylib 217 . . . . . . . . . . 11 (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
4645adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
47 elun1 4135 . . . . . . . . . 10 ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
4846, 47syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
4936, 48eqeltrid 2842 . . . . . . . 8 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
5016, 19, 21, 23, 49addsproplem1 34307 . . . . . . 7 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑙) <s ( 0s +s 𝑙))))
5150simpld 495 . . . . . 6 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No )
52 eleq1a 2833 . . . . . 6 ((𝑙 +s 𝑌) ∈ No → (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No ))
5351, 52syl 17 . . . . 5 ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No ))
5453rexlimdva 3151 . . . 4 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No ))
5554abssdv 4024 . . 3 (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ⊆ No )
5615adantr 481 . . . . . . . 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 481 . . . . . . . 8 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑋 ∈ No )
59 leftssno 27206 . . . . . . . . . 10 ( L ‘𝑌) ⊆ No
6059sseli 3939 . . . . . . . . 9 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ No )
6160adantl 482 . . . . . . . 8 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑚 ∈ No )
6222a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 0s ∈ No )
6324oveq2i 7365 . . . . . . . . . . . 12 (( bday ‘𝑋) +no ( bday ‘ 0s )) = (( bday ‘𝑋) +no ∅)
64 naddid1 8626 . . . . . . . . . . . . 13 (( bday ‘𝑋) ∈ On → (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋))
6539, 64ax-mp 5 . . . . . . . . . . . 12 (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋)
6663, 65eqtri 2764 . . . . . . . . . . 11 (( bday ‘𝑋) +no ( bday ‘ 0s )) = ( bday ‘𝑋)
6766uneq2i 4119 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋))
68 bdayelon 27112 . . . . . . . . . . . 12 ( bday ‘𝑚) ∈ On
69 naddword1 8633 . . . . . . . . . . . 12 ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚)))
7039, 68, 69mp2an 690 . . . . . . . . . . 11 ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚))
71 ssequn2 4142 . . . . . . . . . . 11 (( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚)))
7270, 71mpbi 229 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚))
7367, 72eqtri 2764 . . . . . . . . 9 ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) = (( bday ‘𝑋) +no ( bday ‘𝑚))
74 leftssold 27204 . . . . . . . . . . . . . 14 ( L ‘𝑌) ⊆ ( O ‘( bday ‘𝑌))
7574sseli 3939 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday ‘𝑌)))
76 oldbday 27226 . . . . . . . . . . . . . 14 ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No ) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
7731, 60, 76sylancr 587 . . . . . . . . . . . . 13 (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
7875, 77mpbid 231 . . . . . . . . . . . 12 (𝑚 ∈ ( L ‘𝑌) → ( bday ‘𝑚) ∈ ( bday ‘𝑌))
79 naddel2 8630 . . . . . . . . . . . . 13 ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
8068, 31, 39, 79mp3an 1461 . . . . . . . . . . . 12 (( bday ‘𝑚) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
8178, 80sylib 217 . . . . . . . . . . 11 (𝑚 ∈ ( L ‘𝑌) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
8281adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
83 elun1 4135 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
8482, 83syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
8573, 84eqeltrid 2842 . . . . . . . 8 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
8656, 58, 61, 62, 85addsproplem1 34307 . . . . . . 7 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
8786simpld 495 . . . . . 6 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No )
88 eleq1a 2833 . . . . . 6 ((𝑋 +s 𝑚) ∈ No → (𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No ))
8987, 88syl 17 . . . . 5 ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No ))
9089rexlimdva 3151 . . . 4 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No ))
9190abssdv 4024 . . 3 (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No )
9255, 91unssd 4145 . 2 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ⊆ No )
9315adantr 481 . . . . . . . 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 27207 . . . . . . . . . 10 ( R ‘𝑋) ⊆ No
9594sseli 3939 . . . . . . . . 9 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ No )
9695adantl 482 . . . . . . . 8 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑟 ∈ No )
9720adantr 481 . . . . . . . 8 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑌 ∈ No )
9822a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 0s ∈ No )
9924oveq2i 7365 . . . . . . . . . . . 12 (( bday ‘𝑟) +no ( bday ‘ 0s )) = (( bday ‘𝑟) +no ∅)
100 bdayelon 27112 . . . . . . . . . . . . 13 ( bday ‘𝑟) ∈ On
101 naddid1 8626 . . . . . . . . . . . . 13 (( bday ‘𝑟) ∈ On → (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟))
102100, 101ax-mp 5 . . . . . . . . . . . 12 (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟)
10399, 102eqtri 2764 . . . . . . . . . . 11 (( bday ‘𝑟) +no ( bday ‘ 0s )) = ( bday ‘𝑟)
104103uneq2i 4119 . . . . . . . . . 10 ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟))
105 naddword1 8633 . . . . . . . . . . . 12 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌)))
106100, 31, 105mp2an 690 . . . . . . . . . . 11 ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌))
107 ssequn2 4142 . . . . . . . . . . 11 (( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌)))
108106, 107mpbi 229 . . . . . . . . . 10 ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌))
109104, 108eqtri 2764 . . . . . . . . 9 ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) = (( bday ‘𝑟) +no ( bday ‘𝑌))
110 rightssold 27205 . . . . . . . . . . . . . 14 ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
111110sseli 3939 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday ‘𝑋)))
112 oldbday 27226 . . . . . . . . . . . . . 14 ((( bday ‘𝑋) ∈ On ∧ 𝑟 ∈ No ) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
11339, 95, 112sylancr 587 . . . . . . . . . . . . 13 (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
114111, 113mpbid 231 . . . . . . . . . . . 12 (𝑟 ∈ ( R ‘𝑋) → ( bday ‘𝑟) ∈ ( bday ‘𝑋))
115 naddel1 8629 . . . . . . . . . . . . 13 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
116100, 39, 31, 115mp3an 1461 . . . . . . . . . . . 12 (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
117114, 116sylib 217 . . . . . . . . . . 11 (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
118117adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
119 elun1 4135 . . . . . . . . . 10 ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
120118, 119syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
121109, 120eqeltrid 2842 . . . . . . . 8 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
12293, 96, 97, 98, 121addsproplem1 34307 . . . . . . 7 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
123122simpld 495 . . . . . 6 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No )
124 eleq1a 2833 . . . . . 6 ((𝑟 +s 𝑌) ∈ No → (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No ))
125123, 124syl 17 . . . . 5 ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No ))
126125rexlimdva 3151 . . . 4 (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No ))
127126abssdv 4024 . . 3 (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ⊆ No )
12815adantr 481 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
12957adantr 481 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑋 ∈ No )
130 rightssno 27207 . . . . . . . . . 10 ( R ‘𝑌) ⊆ No
131130sseli 3939 . . . . . . . . 9 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ No )
132131adantl 482 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑠 ∈ No )
13322a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 0s ∈ No )
13466uneq2i 4119 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋))
135 bdayelon 27112 . . . . . . . . . . . 12 ( bday ‘𝑠) ∈ On
136 naddword1 8633 . . . . . . . . . . . 12 ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠)))
13739, 135, 136mp2an 690 . . . . . . . . . . 11 ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠))
138 ssequn2 4142 . . . . . . . . . . 11 (( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠)))
139137, 138mpbi 229 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠))
140134, 139eqtri 2764 . . . . . . . . 9 ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) = (( bday ‘𝑋) +no ( bday ‘𝑠))
141 rightssold 27205 . . . . . . . . . . . . . 14 ( R ‘𝑌) ⊆ ( O ‘( bday ‘𝑌))
142141sseli 3939 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday ‘𝑌)))
143 oldbday 27226 . . . . . . . . . . . . . 14 ((( bday ‘𝑌) ∈ On ∧ 𝑠 ∈ No ) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
14431, 131, 143sylancr 587 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
145142, 144mpbid 231 . . . . . . . . . . . 12 (𝑠 ∈ ( R ‘𝑌) → ( bday ‘𝑠) ∈ ( bday ‘𝑌))
146 naddel2 8630 . . . . . . . . . . . . 13 ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
147135, 31, 39, 146mp3an 1461 . . . . . . . . . . . 12 (( bday ‘𝑠) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
148145, 147sylib 217 . . . . . . . . . . 11 (𝑠 ∈ ( R ‘𝑌) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
149148adantl 482 . . . . . . . . . 10 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
150 elun1 4135 . . . . . . . . . 10 ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
151149, 150syl 17 . . . . . . . . 9 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
152140, 151eqeltrid 2842 . . . . . . . 8 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
153128, 129, 132, 133, 152addsproplem1 34307 . . . . . . 7 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑋) <s ( 0s +s 𝑋))))
154153simpld 495 . . . . . 6 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No )
155 eleq1a 2833 . . . . . 6 ((𝑋 +s 𝑠) ∈ No → (𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No ))
156154, 155syl 17 . . . . 5 ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No ))
157156rexlimdva 3151 . . . 4 (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No ))
158157abssdv 4024 . . 3 (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No )
159127, 158unssd 4145 . 2 (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No )
160 elun 4107 . . . . . . 7 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}))
161 vex 3448 . . . . . . . . 9 𝑎 ∈ V
162 eqeq1 2740 . . . . . . . . . 10 (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌)))
163162rexbidv 3174 . . . . . . . . 9 (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)))
164161, 163elab 3629 . . . . . . . 8 (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))
165 eqeq1 2740 . . . . . . . . . 10 (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚)))
166165rexbidv 3174 . . . . . . . . 9 (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
167161, 166elab 3629 . . . . . . . 8 (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))
168164, 167orbi12i 913 . . . . . . 7 ((𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
169160, 168bitri 274 . . . . . 6 (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)))
170 elun 4107 . . . . . . 7 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
171 vex 3448 . . . . . . . . 9 𝑏 ∈ V
172 eqeq1 2740 . . . . . . . . . 10 (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌)))
173172rexbidv 3174 . . . . . . . . 9 (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
174171, 173elab 3629 . . . . . . . 8 (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))
175 eqeq1 2740 . . . . . . . . . 10 (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠)))
176175rexbidv 3174 . . . . . . . . 9 (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
177171, 176elab 3629 . . . . . . . 8 (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))
178174, 177orbi12i 913 . . . . . . 7 ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
179170, 178bitri 274 . . . . . 6 (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
180169, 179anbi12i 627 . . . . 5 ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) ↔ ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))))
181 anddi 1009 . . . . 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 274 . . . 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 3216 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
184 lltropt 27198 . . . . . . . . . . . . 13 (𝑋 ∈ No → ( L ‘𝑋) <<s ( R ‘𝑋))
18557, 184syl 17 . . . . . . . . . . . 12 (𝜑 → ( L ‘𝑋) <<s ( R ‘𝑋))
186185adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
187 simprl 769 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
188 simprr 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
189186, 187, 188ssltsepcd 27129 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟)
19015adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
19120adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No )
19218ad2antrl 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ No )
19395ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
194 naddcom 8625 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌)))
19531, 26, 194mp2an 690 . . . . . . . . . . . . . . 15 (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌))
19645ad2antrl 726 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
197195, 196eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
198 naddcom 8625 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌)))
19931, 100, 198mp2an 690 . . . . . . . . . . . . . . 15 (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌))
200117ad2antll 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
201199, 200eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
202 naddcl 8620 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On)
20331, 26, 202mp2an 690 . . . . . . . . . . . . . . 15 (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On
204 naddcl 8620 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On)
20531, 100, 204mp2an 690 . . . . . . . . . . . . . . 15 (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On
206 naddcl 8620 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On)
20739, 31, 206mp2an 690 . . . . . . . . . . . . . . 15 (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On
208 onunel 34189 . . . . . . . . . . . . . . 15 (((( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On ∧ (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
209203, 205, 207, 208mp3an 1461 . . . . . . . . . . . . . 14 (((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
210197, 201, 209sylanbrc 583 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
211 elun1 4135 . . . . . . . . . . . . 13 (((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
212210, 211syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
213190, 191, 192, 193, 212addsproplem1 34307 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))))
214213simprd 496 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
215189, 214mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))
216 breq12 5109 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))
217215, 216syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
218217rexlimdvva 3204 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
219183, 218biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
220 reeanv 3216 . . . . . . 7 (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
22151adantrr 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No )
22215adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
22318ad2antrl 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 ∈ No )
224131ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
22522a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s ∈ No )
22629uneq2i 4119 . . . . . . . . . . . . . 14 ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙))
227 naddword1 8633 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠)))
22826, 135, 227mp2an 690 . . . . . . . . . . . . . . 15 ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠))
229 ssequn2 4142 . . . . . . . . . . . . . . 15 (( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠)))
230228, 229mpbi 229 . . . . . . . . . . . . . 14 ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠))
231226, 230eqtri 2764 . . . . . . . . . . . . 13 ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) = (( bday ‘𝑙) +no ( bday ‘𝑠))
232 naddel1 8629 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠))))
23326, 39, 135, 232mp3an 1461 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
23442, 233sylib 217 . . . . . . . . . . . . . . . 16 (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
235234ad2antrl 726 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
236148ad2antll 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
237 ontr1 6362 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On → (((( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
238207, 237ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
239235, 236, 238syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
240 elun1 4135 . . . . . . . . . . . . . 14 ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
241239, 240syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
242231, 241eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
243222, 223, 224, 225, 242addsproplem1 34307 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No ∧ (𝑠 <s 0s → (𝑠 +s 𝑙) <s ( 0s +s 𝑙))))
244243simpld 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No )
245154adantrl 714 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No )
246 rightval 27190 . . . . . . . . . . . . . . 15 ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑠}
247246rabeq2i 3428 . . . . . . . . . . . . . 14 (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑌 <s 𝑠))
248247simprbi 497 . . . . . . . . . . . . 13 (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
249248ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
25020adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 ∈ No )
25145ad2antrl 726 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
252 naddcl 8620 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On)
25326, 31, 252mp2an 690 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On
254 naddcl 8620 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On)
25526, 135, 254mp2an 690 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On
256 onunel 34189 . . . . . . . . . . . . . . . . 17 (((( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On ∧ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
257253, 255, 207, 256mp3an 1461 . . . . . . . . . . . . . . . 16 (((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
258251, 239, 257sylanbrc 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
259 elun1 4135 . . . . . . . . . . . . . . 15 (((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
260258, 259syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
261222, 223, 250, 224, 260addsproplem1 34307 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))))
262261simprd 496 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))
263249, 262mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))
264223, 250addscomd 34305 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙))
265223, 224addscomd 34305 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙))
266263, 264, 2653brtr4d 5136 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠))
267 leftval 27189 . . . . . . . . . . . . . 14 ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑙 <s 𝑋}
268267rabeq2i 3428 . . . . . . . . . . . . 13 (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑙 <s 𝑋))
269268simprbi 497 . . . . . . . . . . . 12 (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
270269ad2antrl 726 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
27157adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No )
272 naddcom 8625 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠)))
273135, 26, 272mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠))
274273, 239eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
275 naddcom 8625 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠)))
276135, 39, 275mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠))
277276, 236eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
278 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On)
279135, 26, 278mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On
280 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On)
281135, 39, 280mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On
282 onunel 34189 . . . . . . . . . . . . . . . 16 (((( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On ∧ (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
283279, 281, 207, 282mp3an 1461 . . . . . . . . . . . . . . 15 (((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
284274, 277, 283sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
285 elun1 4135 . . . . . . . . . . . . . 14 (((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
286284, 285syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
287222, 224, 223, 271, 286addsproplem1 34307 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No ∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))))
288287simprd 496 . . . . . . . . . . 11 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))
289270, 288mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))
290221, 244, 245, 266, 289slttrd 27103 . . . . . . . . 9 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))
291 breq12 5109 . . . . . . . . 9 ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)))
292290, 291syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
293292rexlimdvva 3204 . . . . . . 7 (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
294220, 293biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
295219, 294jaod 857 . . . . 5 (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
296 reeanv 3216 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)))
29715adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
29857adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 ∈ No )
29960ad2antrl 726 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ No )
30022a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s ∈ No )
30181ad2antrl 726 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
302301, 83syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
30373, 302eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
304297, 298, 299, 300, 303addsproplem1 34307 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑋) <s ( 0s +s 𝑋))))
305304simpld 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No )
30695ad2antll 727 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
307103uneq2i 4119 . . . . . . . . . . . . . 14 ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟))
308 naddword1 8633 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚)))
309100, 68, 308mp2an 690 . . . . . . . . . . . . . . 15 ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚))
310 ssequn2 4142 . . . . . . . . . . . . . . 15 (( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚)))
311309, 310mpbi 229 . . . . . . . . . . . . . 14 ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚))
312307, 311eqtri 2764 . . . . . . . . . . . . 13 ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) = (( bday ‘𝑟) +no ( bday ‘𝑚))
313 naddel1 8629 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚))))
314100, 39, 68, 313mp3an 1461 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
315114, 314sylib 217 . . . . . . . . . . . . . . . 16 (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
316315ad2antll 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
317 ontr1 6362 . . . . . . . . . . . . . . . 16 ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On → (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
318207, 317ax-mp 5 . . . . . . . . . . . . . . 15 (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
319316, 301, 318syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
320 elun1 4135 . . . . . . . . . . . . . 14 ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
321319, 320syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
322312, 321eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
323297, 306, 299, 300, 322addsproplem1 34307 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 0s → (𝑚 +s 𝑟) <s ( 0s +s 𝑟))))
324323simpld 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No )
32520adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No )
326117ad2antll 727 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
327326, 119syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
328109, 327eqeltrid 2842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
329297, 306, 325, 300, 328addsproplem1 34307 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No ∧ (𝑌 <s 0s → (𝑌 +s 𝑟) <s ( 0s +s 𝑟))))
330329simpld 495 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No )
331 rightval 27190 . . . . . . . . . . . . . . . 16 ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟}
332331eleq2i 2829 . . . . . . . . . . . . . . 15 (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
333332biimpi 215 . . . . . . . . . . . . . 14 (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
334333ad2antll 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
335 rabid 3426 . . . . . . . . . . . . 13 (𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑟))
336334, 335sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑟))
337336simprd 496 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
338 naddcom 8625 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚)))
33968, 39, 338mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚))
340339, 301eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
341 naddcom 8625 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚)))
34268, 100, 341mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚))
343342, 319eqeltrid 2842 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
344 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On)
34568, 39, 344mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On
346 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On)
34768, 100, 346mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On
348 onunel 34189 . . . . . . . . . . . . . . . 16 (((( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On ∧ (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
349345, 347, 207, 348mp3an 1461 . . . . . . . . . . . . . . 15 (((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
350340, 343, 349sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
351 elun1 4135 . . . . . . . . . . . . . 14 (((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
352350, 351syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
353297, 299, 298, 306, 352addsproplem1 34307 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No ∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))))
354353simprd 496 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))
355337, 354mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))
356 leftval 27189 . . . . . . . . . . . . . . . . 17 ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌}
357356eleq2i 2829 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
358357biimpi 215 . . . . . . . . . . . . . . 15 (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
359358ad2antrl 726 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
360 rabid 3426 . . . . . . . . . . . . . 14 (𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑚 <s 𝑌))
361359, 360sylib 217 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑚 <s 𝑌))
362361simprd 496 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
363 naddcl 8620 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On)
364100, 68, 363mp2an 690 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On
365 naddcl 8620 . . . . . . . . . . . . . . . . . 18 ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On)
366100, 31, 365mp2an 690 . . . . . . . . . . . . . . . . 17 (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On
367 onunel 34189 . . . . . . . . . . . . . . . . 17 (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On ∧ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
368364, 366, 207, 367mp3an 1461 . . . . . . . . . . . . . . . 16 (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
369319, 326, 368sylanbrc 583 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
370 elun1 4135 . . . . . . . . . . . . . . 15 (((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
371369, 370syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
372297, 306, 299, 325, 371addsproplem1 34307 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))))
373372simprd 496 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))
374362, 373mpd 15 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))
375306, 299addscomd 34305 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟))
376306, 325addscomd 34305 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟))
377374, 375, 3763brtr4d 5136 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌))
378305, 324, 330, 355, 377slttrd 27103 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))
379 breq12 5109 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)))
380378, 379syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
381380rexlimdvva 3204 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
382296, 381biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏))
383 reeanv 3216 . . . . . . 7 (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))
384 lltropt 27198 . . . . . . . . . . . . . 14 (𝑌 ∈ No → ( L ‘𝑌) <<s ( R ‘𝑌))
38520, 384syl 17 . . . . . . . . . . . . 13 (𝜑 → ( L ‘𝑌) <<s ( R ‘𝑌))
386385adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
387 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
388 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
389386, 387, 388ssltsepcd 27129 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠)
39015adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No ∀𝑦 ∈ No ∀𝑧 ∈ No (((( bday ‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday ‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
39157adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No )
39260ad2antrl 726 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ No )
393131ad2antll 727 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
39481ad2antrl 726 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
395148ad2antll 727 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
396 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On)
39739, 68, 396mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On
398 naddcl 8620 . . . . . . . . . . . . . . . . 17 ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On)
39939, 135, 398mp2an 690 . . . . . . . . . . . . . . . 16 (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On
400 onunel 34189 . . . . . . . . . . . . . . . 16 (((( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On ∧ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On) → (((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))))
401397, 399, 207, 400mp3an 1461 . . . . . . . . . . . . . . 15 (((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∧ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
402394, 395, 401sylanbrc 583 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
403 elun1 4135 . . . . . . . . . . . . . 14 (((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
404402, 403syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
405390, 391, 392, 393, 404addsproplem1 34307 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No ∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))))
406405simprd 496 . . . . . . . . . . 11 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))
407389, 406mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))
408391, 392addscomd 34305 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋))
409391, 393addscomd 34305 . . . . . . . . . 10 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋))
410407, 408, 4093brtr4d 5136 . . . . . . . . 9 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))
411 breq12 5109 . . . . . . . . 9 ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)))
412410, 411syl5ibrcom 246 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
413412rexlimdvva 3204 . . . . . . 7 (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
414383, 413biimtrrid 242 . . . . . 6 (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏))
415382, 414jaod 857 . . . . 5 (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏))
416295, 415jaod 857 . . . 4 (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏))
417182, 416biimtrid 241 . . 3 (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏))
4184173impib 1116 . 2 ((𝜑 ∧ 𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)
4197, 14, 92, 159, 418ssltd 27127 1 (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106  {cab 2713  ∀wral 3063  ∃wrex 3072  {crab 3406  Vcvv 3444   ∪ cun 3907   ⊆ wss 3909  ∅c0 4281   class class class wbr 5104  Oncon0 6316  ‘cfv 6494  (class class class)co 7354   +no cnadd 8608   No csur 26984   <s cslt 26985   bday cbday 26986   <<s csslt 27116   0s c0s 27157   O cold 27169   L cleft 27171   R cright 27172   +s cadds 34297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7669
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2888  df-ne 2943  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-int 4907  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5530  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5587  df-se 5588  df-we 5589  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6252  df-ord 6319  df-on 6320  df-suc 6322  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7310  df-ov 7357  df-oprab 7358  df-mpo 7359  df-1st 7918  df-2nd 7919  df-frecs 8209  df-wrecs 8240  df-recs 8314  df-1o 8409  df-2o 8410  df-nadd 8609  df-no 26987  df-slt 26988  df-bday 26989  df-sslt 27117  df-scut 27119  df-0s 27159  df-made 27173  df-old 27174  df-left 27176  df-right 27177  df-norec2 27257  df-adds 34298
This theorem is referenced by:  addsproplem3  34309
  Copyright terms: Public domain W3C validator