Metamath Proof Explorer

Theorem addsproplem6

Description: Lemma for surreal addition properties. Finally, we show the second half of the induction hypothesis when Y and Z are the same age. (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 𝑥 ) ) ) ) )
addspropord.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
addspropord.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
addspropord.4 ⊢ ( 𝜑 → 𝑍 ∈ No )
addspropord.5 ⊢ ( 𝜑 → 𝑌 <s 𝑍 )
addsproplem6.6 ⊢ ( 𝜑 → ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) )
Assertion addsproplem6 ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +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 addspropord.2 ⊢ ( 𝜑 → 𝑋 ∈ No )
3 addspropord.3 ⊢ ( 𝜑 → 𝑌 ∈ No )
4 addspropord.4 ⊢ ( 𝜑 → 𝑍 ∈ No )
5 addspropord.5 ⊢ ( 𝜑 → 𝑌 <s 𝑍 )
6 addsproplem6.6 ⊢ ( 𝜑 → ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) )
7 nodense ⊢ ( ( ( 𝑌 ∈ No ∧ 𝑍 ∈ No ) ∧ ( ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) ∧ 𝑌 <s 𝑍 ) ) → ∃ 𝑚 ∈ No ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) )
8 3 4 6 5 7 syl22anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ No ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) )
9 1 2 3 addsproplem3 ⊢ ( 𝜑 → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) ) )
10 9 simp1d ⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ No )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑌 ) ∈ No )
12 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑋 ∈ No )
14 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 ∈ No )
15 unidm ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
16 simprr1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) )
17 bdayelon ⊢ ( bday ‘ 𝑚 ) ∈ On
18 bdayelon ⊢ ( bday ‘ 𝑌 ) ∈ On
19 bdayelon ⊢ ( bday ‘ 𝑋 ) ∈ On
20 naddel2 ⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
21 17 18 19 20 mp3an ⊢ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
22 16 21 sylib ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
23 elun1 ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
24 22 23 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
25 15 24 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
26 12 13 14 14 25 addsproplem1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑚 → ( 𝑚 +s 𝑋 ) <s ( 𝑚 +s 𝑋 ) ) ) )
27 26 simpld ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
28 uncom ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
29 28 eleq2i ⊢ ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ↔ ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
30 29 imbi1i ⊢ ( ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ↔ ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
31 30 ralbii ⊢ ( ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ↔ ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
32 31 2ralbii ⊢ ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
33 1 32 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
34 33 2 4 addsproplem3 ⊢ ( 𝜑 → ( ( 𝑋 +s 𝑍 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑍 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑍 ) } ∧ { ( 𝑋 +s 𝑍 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑍 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑍 ) 𝑔 = ( 𝑋 +s ℎ ) } ) ) )
35 34 simp1d ⊢ ( 𝜑 → ( 𝑋 +s 𝑍 ) ∈ No )
36 35 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑍 ) ∈ No )
37 9 simp3d ⊢ ( 𝜑 → { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) )
39 ovex ⊢ ( 𝑋 +s 𝑌 ) ∈ V
40 39 snid ⊢ ( 𝑋 +s 𝑌 ) ∈ { ( 𝑋 +s 𝑌 ) }
41 40 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑌 ) ∈ { ( 𝑋 +s 𝑌 ) } )
42 oldbday ⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑚 ∈ No ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
43 18 14 42 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
44 16 43 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
45 simprr2 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑌 <s 𝑚 )
46 breq2 ⊢ ( 𝑎 = 𝑚 → ( 𝑌 <s 𝑎 ↔ 𝑌 <s 𝑚 ) )
47 rightval ⊢ ( R ‘ 𝑌 ) = { 𝑎 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑌 <s 𝑎 }
48 46 47 elrab2 ⊢ ( 𝑚 ∈ ( R ‘ 𝑌 ) ↔ ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑌 <s 𝑚 ) )
49 44 45 48 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 ∈ ( R ‘ 𝑌 ) )
50 eqid ⊢ ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑚 )
51 oveq2 ⊢ ( ℎ = 𝑚 → ( 𝑋 +s ℎ ) = ( 𝑋 +s 𝑚 ) )
52 51 rspceeqv ⊢ ( ( 𝑚 ∈ ( R ‘ 𝑌 ) ∧ ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑚 ) ) → ∃ ℎ ∈ ( R ‘ 𝑌 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s ℎ ) )
53 49 50 52 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ∃ ℎ ∈ ( R ‘ 𝑌 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s ℎ ) )
54 ovex ⊢ ( 𝑋 +s 𝑚 ) ∈ V
55 eqeq1 ⊢ ( 𝑔 = ( 𝑋 +s 𝑚 ) → ( 𝑔 = ( 𝑋 +s ℎ ) ↔ ( 𝑋 +s 𝑚 ) = ( 𝑋 +s ℎ ) ) )
56 55 rexbidv ⊢ ( 𝑔 = ( 𝑋 +s 𝑚 ) → ( ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) ↔ ∃ ℎ ∈ ( R ‘ 𝑌 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s ℎ ) ) )
57 54 56 elab ⊢ ( ( 𝑋 +s 𝑚 ) ∈ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ↔ ∃ ℎ ∈ ( R ‘ 𝑌 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s ℎ ) )
58 53 57 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } )
59 elun2 ⊢ ( ( 𝑋 +s 𝑚 ) ∈ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } → ( 𝑋 +s 𝑚 ) ∈ ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) )
61 38 41 60 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑌 ) <s ( 𝑋 +s 𝑚 ) )
62 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
63 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑍 ∈ No )
64 62 13 63 addsproplem3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( ( 𝑋 +s 𝑍 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑍 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑍 ) } ∧ { ( 𝑋 +s 𝑍 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑍 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑍 ) 𝑔 = ( 𝑋 +s ℎ ) } ) ) )
65 64 simp2d ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑍 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑍 ) } )
66 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( bday ‘ 𝑌 ) = ( bday ‘ 𝑍 ) )
67 16 66 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑍 ) )
68 bdayelon ⊢ ( bday ‘ 𝑍 ) ∈ On
69 oldbday ⊢ ( ( ( bday ‘ 𝑍 ) ∈ On ∧ 𝑚 ∈ No ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑍 ) ) )
70 68 14 69 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑍 ) ) )
71 67 70 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) )
72 simprr3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 <s 𝑍 )
73 breq1 ⊢ ( 𝑎 = 𝑚 → ( 𝑎 <s 𝑍 ↔ 𝑚 <s 𝑍 ) )
74 leftval ⊢ ( L ‘ 𝑍 ) = { 𝑎 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ∣ 𝑎 <s 𝑍 }
75 73 74 elrab2 ⊢ ( 𝑚 ∈ ( L ‘ 𝑍 ) ↔ ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ∧ 𝑚 <s 𝑍 ) )
76 71 72 75 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → 𝑚 ∈ ( L ‘ 𝑍 ) )
77 oveq2 ⊢ ( 𝑑 = 𝑚 → ( 𝑋 +s 𝑑 ) = ( 𝑋 +s 𝑚 ) )
78 77 rspceeqv ⊢ ( ( 𝑚 ∈ ( L ‘ 𝑍 ) ∧ ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑚 ) ) → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) )
79 76 50 78 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) )
80 eqeq1 ⊢ ( 𝑐 = ( 𝑋 +s 𝑚 ) → ( 𝑐 = ( 𝑋 +s 𝑑 ) ↔ ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) ) )
81 80 rexbidv ⊢ ( 𝑐 = ( 𝑋 +s 𝑚 ) → ( ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) ) )
82 54 81 elab ⊢ ( ( 𝑋 +s 𝑚 ) ∈ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) )
83 79 82 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } )
84 elun2 ⊢ ( ( 𝑋 +s 𝑚 ) ∈ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } → ( 𝑋 +s 𝑚 ) ∈ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑍 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) )
85 83 84 syl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑍 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) )
86 ovex ⊢ ( 𝑋 +s 𝑍 ) ∈ V
87 86 snid ⊢ ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) }
88 87 a1i ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) } )
89 65 85 88 ssltsepcd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑍 ) )
90 11 27 36 61 89 slttrd ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ No ∧ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ∧ 𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍 ) ) ) → ( 𝑋 +s 𝑌 ) <s ( 𝑋 +s 𝑍 ) )
91 8 90 rexlimddv ⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) <s ( 𝑋 +s 𝑍 ) )
92 3 2 addscomd ⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) = ( 𝑋 +s 𝑌 ) )
93 4 2 addscomd ⊢ ( 𝜑 → ( 𝑍 +s 𝑋 ) = ( 𝑋 +s 𝑍 ) )
94 91 92 93 3brtr4d ⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )