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