Metamath Proof Explorer

Theorem addsproplem4

Description: Lemma for surreal addition properties. Show the second half of the inductive hypothesis when Y is older than Z . (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 𝑍 )
addsproplem4.6 ⊢ ( 𝜑 → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) )
Assertion addsproplem4 ( 𝜑 → ( 𝑌 +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 addsproplem4.6 ⊢ ( 𝜑 → ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) )
7 uncom ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
8 7 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 ‘ 𝑌 ) ) ) )
9 8 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 𝑥 ) ) ) ) )
10 9 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 𝑥 ) ) ) ) )
11 10 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 𝑥 ) ) ) ) )
12 1 11 sylib ⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
13 12 2 4 addsproplem3 ⊢ ( 𝜑 → ( ( 𝑋 +s 𝑍 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑍 ) } ∧ { ( 𝑋 +s 𝑍 ) } <<s ( { 𝑒 ∣ ∃ 𝑔 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑔 +s 𝑍 ) } ∪ { 𝑓 ∣ ∃ ℎ ∈ ( R ‘ 𝑍 ) 𝑓 = ( 𝑋 +s ℎ ) } ) ) )
14 13 simp2d ⊢ ( 𝜑 → ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑍 ) } )
15 bdayelon ⊢ ( bday ‘ 𝑍 ) ∈ On
16 oldbday ⊢ ( ( ( bday ‘ 𝑍 ) ∈ On ∧ 𝑌 ∈ No ) → ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ↔ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) )
17 15 3 16 sylancr ⊢ ( 𝜑 → ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ↔ ( bday ‘ 𝑌 ) ∈ ( bday ‘ 𝑍 ) ) )
18 6 17 mpbird ⊢ ( 𝜑 → 𝑌 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) )
19 elleft ⊢ ( 𝑌 ∈ ( L ‘ 𝑍 ) ↔ ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ∧ 𝑌 <s 𝑍 ) )
20 18 5 19 sylanbrc ⊢ ( 𝜑 → 𝑌 ∈ ( L ‘ 𝑍 ) )
21 eqid ⊢ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑌 )
22 oveq2 ⊢ ( 𝑑 = 𝑌 → ( 𝑋 +s 𝑑 ) = ( 𝑋 +s 𝑌 ) )
23 22 rspceeqv ⊢ ( ( 𝑌 ∈ ( L ‘ 𝑍 ) ∧ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑌 ) ) → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
24 20 21 23 sylancl ⊢ ( 𝜑 → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
25 ovex ⊢ ( 𝑋 +s 𝑌 ) ∈ V
26 eqeq1 ⊢ ( 𝑏 = ( 𝑋 +s 𝑌 ) → ( 𝑏 = ( 𝑋 +s 𝑑 ) ↔ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) ) )
27 26 rexbidv ⊢ ( 𝑏 = ( 𝑋 +s 𝑌 ) → ( ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) ) )
28 25 27 elab ⊢ ( ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
29 24 28 sylibr ⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } )
30 elun2 ⊢ ( ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } → ( 𝑋 +s 𝑌 ) ∈ ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) )
31 29 30 syl ⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) )
32 ovex ⊢ ( 𝑋 +s 𝑍 ) ∈ V
33 32 snid ⊢ ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) }
34 33 a1i ⊢ ( 𝜑 → ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) } )
35 14 31 34 ssltsepcd ⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) <s ( 𝑋 +s 𝑍 ) )
36 3 2 addscomd ⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) = ( 𝑋 +s 𝑌 ) )
37 4 2 addscomd ⊢ ( 𝜑 → ( 𝑍 +s 𝑋 ) = ( 𝑋 +s 𝑍 ) )
38 35 36 37 3brtr4d ⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )