Metamath Proof Explorer

Theorem addsproplem2

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)

Ref Expression
Hypotheses 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 addsproplem2 ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )

Proof

Step Hyp Ref Expression
1 addsproplem.1 ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
2 addsproplem2.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
3 addsproplem2.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
4 fvex ⊢ ( L ‘ 𝑋 ) ∈ V
5 4 abrexex ⊢ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V
6 5 a1i ⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V )
7 fvex ⊢ ( L ‘ 𝑌 ) ∈ V
8 7 abrexex ⊢ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V
9 8 a1i ⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V )
10 6 9 unexd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∈ V )
11 fvex ⊢ ( R ‘ 𝑋 ) ∈ V
12 11 abrexex ⊢ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V
13 12 a1i ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V )
14 fvex ⊢ ( R ‘ 𝑌 ) ∈ V
15 14 abrexex ⊢ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V
16 15 a1i ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V )
17 13 16 unexd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ∈ V )
18 1 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
19 leftno ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ No )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑙 ∈ No )
21 3 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑌 ∈ No )
22 0no ⊢ 0s ∈ No
23 22 a1i ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 0s ∈ No )
24 bday0 ⊢ ( bday ‘ 0s ) = ∅
25 24 oveq2i ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑙 ) +no ∅ )
26 bdayon ⊢ ( bday ‘ 𝑙 ) ∈ On
27 naddrid ⊢ ( ( bday ‘ 𝑙 ) ∈ On → ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 ) )
28 26 27 ax-mp ⊢ ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 )
29 25 28 eqtri ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑙 )
30 29 uneq2i ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) )
31 bdayon ⊢ ( bday ‘ 𝑌 ) ∈ On
32 naddword1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
33 26 31 32 mp2an ⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
34 ssequn2 ⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
35 33 34 mpbi ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
36 30 35 eqtri ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
37 leftold ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
38 bdayon ⊢ ( bday ‘ 𝑋 ) ∈ On
39 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑙 ∈ No ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
40 38 19 39 sylancr ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
41 37 40 mpbid ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) )
42 naddel1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
43 26 38 31 42 mp3an ⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
44 41 43 sylib ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
46 elun1 ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
48 36 47 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
49 18 20 21 23 48 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
50 49 simpld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
51 eleq1a ⊢ ( ( 𝑙 +s 𝑌 ) ∈ No → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
52 50 51 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
53 52 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
54 53 abssdv ⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ⊆ No )
55 1 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
56 2 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑋 ∈ No )
57 leftno ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ No )
58 57 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑚 ∈ No )
59 22 a1i ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 0s ∈ No )
60 24 oveq2i ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑋 ) +no ∅ )
61 naddrid ⊢ ( ( bday ‘ 𝑋 ) ∈ On → ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 ) )
62 38 61 ax-mp ⊢ ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 )
63 60 62 eqtri ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑋 )
64 63 uneq2i ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) )
65 bdayon ⊢ ( bday ‘ 𝑚 ) ∈ On
66 naddword1 ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
67 38 65 66 mp2an ⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
68 ssequn2 ⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
69 67 68 mpbi ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
70 64 69 eqtri ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
71 leftold ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
72 oldbday ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑚 ∈ No ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
73 31 57 72 sylancr ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
74 71 73 mpbid ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) )
75 naddel2 ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
76 65 31 38 75 mp3an ⊢ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
77 74 76 sylib ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
78 77 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
79 elun1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
80 78 79 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
81 70 80 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
82 55 56 58 59 81 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
83 82 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
84 eleq1a ⊢ ( ( 𝑋 +s 𝑚 ) ∈ No → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
85 83 84 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
86 85 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
87 86 abssdv ⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ⊆ No )
88 54 87 unssd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ⊆ No )
89 1 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
90 rightno ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ No )
91 90 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑟 ∈ No )
92 3 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑌 ∈ No )
93 22 a1i ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 0s ∈ No )
94 24 oveq2i ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑟 ) +no ∅ )
95 bdayon ⊢ ( bday ‘ 𝑟 ) ∈ On
96 naddrid ⊢ ( ( bday ‘ 𝑟 ) ∈ On → ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 ) )
97 95 96 ax-mp ⊢ ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 )
98 94 97 eqtri ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑟 )
99 98 uneq2i ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) )
100 naddword1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
101 95 31 100 mp2an ⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
102 ssequn2 ⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
103 101 102 mpbi ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
104 99 103 eqtri ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
105 rightold ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
106 oldbday ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑟 ∈ No ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
107 38 90 106 sylancr ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
108 105 107 mpbid ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) )
109 naddel1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
110 95 38 31 109 mp3an ⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
111 108 110 sylib ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
112 111 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
113 elun1 ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
114 112 113 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
115 104 114 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
116 89 91 92 93 115 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
117 116 simpld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
118 eleq1a ⊢ ( ( 𝑟 +s 𝑌 ) ∈ No → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
119 117 118 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
120 119 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
121 120 abssdv ⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ⊆ No )
122 1 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
123 2 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑋 ∈ No )
124 rightno ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ No )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑠 ∈ No )
126 22 a1i ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 0s ∈ No )
127 63 uneq2i ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) )
128 bdayon ⊢ ( bday ‘ 𝑠 ) ∈ On
129 naddword1 ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
130 38 128 129 mp2an ⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
131 ssequn2 ⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
132 130 131 mpbi ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
133 127 132 eqtri ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
134 rightold ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
135 oldbday ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑠 ∈ No ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
136 31 124 135 sylancr ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
137 134 136 mpbid ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) )
138 naddel2 ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
139 128 31 38 138 mp3an ⊢ ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
140 137 139 sylib ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
141 140 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
142 elun1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
143 141 142 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
144 133 143 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
145 122 123 125 126 144 addsproplem1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
146 145 simpld ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
147 eleq1a ⊢ ( ( 𝑋 +s 𝑠 ) ∈ No → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
148 146 147 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
149 148 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
150 149 abssdv ⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ⊆ No )
151 121 150 unssd ⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ⊆ No )
152 elun ⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) )
153 vex ⊢ 𝑎 ∈ V
154 eqeq1 ⊢ ( 𝑝 = 𝑎 → ( 𝑝 = ( 𝑙 +s 𝑌 ) ↔ 𝑎 = ( 𝑙 +s 𝑌 ) ) )
155 154 rexbidv ⊢ ( 𝑝 = 𝑎 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ) )
156 153 155 elab ⊢ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) )
157 eqeq1 ⊢ ( 𝑞 = 𝑎 → ( 𝑞 = ( 𝑋 +s 𝑚 ) ↔ 𝑎 = ( 𝑋 +s 𝑚 ) ) )
158 157 rexbidv ⊢ ( 𝑞 = 𝑎 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
159 153 158 elab ⊢ ( 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) )
160 156 159 orbi12i ⊢ ( ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
161 152 160 bitri ⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
162 elun ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )
163 vex ⊢ 𝑏 ∈ V
164 eqeq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 = ( 𝑟 +s 𝑌 ) ↔ 𝑏 = ( 𝑟 +s 𝑌 ) ) )
165 164 rexbidv ⊢ ( 𝑤 = 𝑏 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
166 163 165 elab ⊢ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) )
167 eqeq1 ⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝑋 +s 𝑠 ) ↔ 𝑏 = ( 𝑋 +s 𝑠 ) ) )
168 167 rexbidv ⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
169 163 168 elab ⊢ ( 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) )
170 166 169 orbi12i ⊢ ( ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
171 162 170 bitri ⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
172 161 171 anbi12i ⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) )
173 anddi ⊢ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
174 172 173 bitri ⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
175 reeanv ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
176 lltr ⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
177 176 a1i ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
178 simprl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ ( L ‘ 𝑋 ) )
179 simprr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ ( R ‘ 𝑋 ) )
180 177 178 179 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 <s 𝑟 )
181 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
182 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
183 19 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ No )
184 90 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
185 naddcom ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
186 31 26 185 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
187 44 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
188 186 187 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
189 naddcom ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
190 31 95 189 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
191 111 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
192 190 191 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
193 naddcl ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
194 31 26 193 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On
195 naddcl ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
196 31 95 195 mp2an ⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On
197 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
198 38 31 197 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On
199 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
200 194 196 198 199 mp3an ⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
201 188 192 200 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
202 elun1 ⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
203 201 202 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
204 181 182 183 184 203 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑌 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) ) )
205 204 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
206 180 205 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) )
207 breq12 ⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
208 206 207 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
209 208 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
210 175 209 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
211 reeanv ⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
212 50 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
213 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
214 19 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 ∈ No )
215 124 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
216 22 a1i ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 0s ∈ No )
217 29 uneq2i ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) )
218 naddword1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
219 26 128 218 mp2an ⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
220 ssequn2 ⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
221 219 220 mpbi ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
222 217 221 eqtri ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
223 naddel1 ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) )
224 26 38 128 223 mp3an ⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
225 41 224 sylib ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
226 225 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
227 140 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
228 ontr1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
229 198 228 ax-mp ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
230 226 227 229 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
231 elun1 ⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
232 230 231 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
233 222 232 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
234 213 214 215 216 233 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
235 234 simpld ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) ∈ No )
236 146 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
237 rightgt ⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑌 <s 𝑠 )
238 237 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 <s 𝑠 )
239 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 ∈ No )
240 44 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
241 naddcl ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
242 26 31 241 mp2an ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On
243 naddcl ⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
244 26 128 243 mp2an ⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On
245 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
246 242 244 198 245 mp3an ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
247 240 230 246 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
248 elun1 ⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
249 247 248 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
250 213 214 239 215 249 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) ) )
251 250 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) )
252 238 251 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) )
253 214 239 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) = ( 𝑌 +s 𝑙 ) )
254 214 215 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) = ( 𝑠 +s 𝑙 ) )
255 252 253 254 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑙 +s 𝑠 ) )
256 leftlt ⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 <s 𝑋 )
257 256 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 <s 𝑋 )
258 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
259 naddcom ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
260 128 26 259 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
261 260 230 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
262 naddcom ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
263 128 38 262 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
264 263 227 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
265 naddcl ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
266 128 26 265 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On
267 naddcl ⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
268 128 38 267 mp2an ⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On
269 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
270 266 268 198 269 mp3an ⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
271 261 264 270 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
272 elun1 ⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
273 271 272 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
274 213 215 214 258 273 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑠 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) ) )
275 274 simprd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) )
276 257 275 mpd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) )
277 212 235 236 255 276 ltstrd ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) )
278 breq12 ⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) ) )
279 277 278 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
280 279 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
281 211 280 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
282 210 281 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
283 reeanv ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
284 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
285 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 ∈ No )
286 57 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ No )
287 22 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 0s ∈ No )
288 77 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
289 288 79 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
290 70 289 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
291 284 285 286 287 290 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
292 291 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
293 90 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
294 98 uneq2i ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) )
295 naddword1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
296 95 65 295 mp2an ⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
297 ssequn2 ⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
298 296 297 mpbi ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
299 294 298 eqtri ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
300 naddel1 ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ) )
301 95 38 65 300 mp3an ⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
302 108 301 sylib ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
303 302 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
304 ontr1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
305 198 304 ax-mp ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
306 303 288 305 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
307 elun1 ⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
308 306 307 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
309 299 308 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
310 284 293 286 287 309 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
311 310 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) ∈ No )
312 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
313 111 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
314 313 113 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
315 104 314 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
316 284 293 312 287 315 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
317 316 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
318 rightval ⊢ ( R ‘ 𝑋 ) = { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 }
319 318 eleq2i ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) ↔ 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
320 319 biimpi ⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
321 320 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
322 rabid ⊢ ( 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } ↔ ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
323 321 322 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
324 323 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 <s 𝑟 )
325 naddcom ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
326 65 38 325 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
327 326 288 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
328 naddcom ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
329 65 95 328 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
330 329 306 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
331 naddcl ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
332 65 38 331 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On
333 naddcl ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
334 65 95 333 mp2an ⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On
335 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
336 332 334 198 335 mp3an ⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
337 327 330 336 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
338 elun1 ⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
339 337 338 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
340 284 286 285 293 339 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑚 +s 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) ) )
341 340 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) )
342 324 341 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) )
343 leftval ⊢ ( L ‘ 𝑌 ) = { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 }
344 343 eleq2i ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) ↔ 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
345 344 biimpi ⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
346 345 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
347 rabid ⊢ ( 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } ↔ ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
348 346 347 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
349 348 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 <s 𝑌 )
350 naddcl ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
351 95 65 350 mp2an ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On
352 naddcl ⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
353 95 31 352 mp2an ⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On
354 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
355 351 353 198 354 mp3an ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
356 306 313 355 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
357 elun1 ⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
358 356 357 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
359 284 293 286 312 358 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) ) )
360 359 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) )
361 349 360 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) )
362 293 286 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) = ( 𝑚 +s 𝑟 ) )
363 293 312 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) = ( 𝑌 +s 𝑟 ) )
364 361 362 363 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
365 292 311 317 342 364 ltstrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
366 breq12 ⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) ) )
367 365 366 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
368 367 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
369 283 368 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
370 reeanv ⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
371 lltr ⊢ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 )
372 371 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
373 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ ( L ‘ 𝑌 ) )
374 simprr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ ( R ‘ 𝑌 ) )
375 372 373 374 sltssepcd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 <s 𝑠 )
376 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
377 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
378 57 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ No )
379 124 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
380 77 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
381 140 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
382 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
383 38 65 382 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On
384 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
385 38 128 384 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On
386 onunel ⊢ ( ( ( ( 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 ‘ 𝑌 ) ) ) ) )
387 383 385 198 386 mp3an ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
388 380 381 387 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
389 elun1 ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
390 388 389 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
391 376 377 378 379 390 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) ) )
392 391 simprd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) )
393 375 392 mpd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) )
394 377 378 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) = ( 𝑚 +s 𝑋 ) )
395 377 379 addscomd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) = ( 𝑠 +s 𝑋 ) )
396 393 394 395 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) )
397 breq12 ⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) ) )
398 396 397 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
399 398 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
400 370 399 biimtrrid ⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
401 369 400 jaod ⊢ ( 𝜑 → ( ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
402 282 401 jaod ⊢ ( 𝜑 → ( ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) → 𝑎 <s 𝑏 ) )
403 174 402 biimtrid ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 ) )
404 403 3impib ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 )
405 10 17 88 151 404 sltsd ⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )