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		breq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 <s 𝑍 ↔ 𝑌 <s 𝑍 ) )
20		leftval	⊢ ( L ‘ 𝑍 ) = { 𝑦 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ∣ 𝑦 <s 𝑍 }
21	19 20	elrab2	⊢ ( 𝑌 ∈ ( L ‘ 𝑍 ) ↔ ( 𝑌 ∈ ( O ‘ ( bday ‘ 𝑍 ) ) ∧ 𝑌 <s 𝑍 ) )
22	18 5 21	sylanbrc	⊢ ( 𝜑 → 𝑌 ∈ ( L ‘ 𝑍 ) )
23		eqid	⊢ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑌 )
24		oveq2	⊢ ( 𝑑 = 𝑌 → ( 𝑋 +s 𝑑 ) = ( 𝑋 +s 𝑌 ) )
25	24	rspceeqv	⊢ ( ( 𝑌 ∈ ( L ‘ 𝑍 ) ∧ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑌 ) ) → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
26	22 23 25	sylancl	⊢ ( 𝜑 → ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
27		ovex	⊢ ( 𝑋 +s 𝑌 ) ∈ V
28		eqeq1	⊢ ( 𝑏 = ( 𝑋 +s 𝑌 ) → ( 𝑏 = ( 𝑋 +s 𝑑 ) ↔ ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) ) )
29	28	rexbidv	⊢ ( 𝑏 = ( 𝑋 +s 𝑌 ) → ( ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) ) )
30	27 29	elab	⊢ ( ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ↔ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) ( 𝑋 +s 𝑌 ) = ( 𝑋 +s 𝑑 ) )
31	26 30	sylibr	⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } )
32		elun2	⊢ ( ( 𝑋 +s 𝑌 ) ∈ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } → ( 𝑋 +s 𝑌 ) ∈ ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) )
33	31 32	syl	⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) ∈ ( { 𝑎 ∣ ∃ 𝑐 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑐 +s 𝑍 ) } ∪ { 𝑏 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑍 ) 𝑏 = ( 𝑋 +s 𝑑 ) } ) )
34		ovex	⊢ ( 𝑋 +s 𝑍 ) ∈ V
35	34	snid	⊢ ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) }
36	35	a1i	⊢ ( 𝜑 → ( 𝑋 +s 𝑍 ) ∈ { ( 𝑋 +s 𝑍 ) } )
37	14 33 36	ssltsepcd	⊢ ( 𝜑 → ( 𝑋 +s 𝑌 ) <s ( 𝑋 +s 𝑍 ) )
38	3 2	addscomd	⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) = ( 𝑋 +s 𝑌 ) )
39	4 2	addscomd	⊢ ( 𝜑 → ( 𝑍 +s 𝑋 ) = ( 𝑋 +s 𝑍 ) )
40	37 38 39	3brtr4d	⊢ ( 𝜑 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) )