Theorem addsproplem5

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