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	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\forall z\in \mathrm{No}\left(\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\right)\cup \left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left(z\right)\right)\in \left(\left(\mathrm{bday}\left(X\right)+\mathrm{bday}\left(Y\right)\right)\cup \left(\mathrm{bday}\left(X\right)+\mathrm{bday}\left(Z\right)\right)\right)\to \left(x{+}_{s}y\in \mathrm{No}\wedge \left(y{<}_{s}z\to \left(y{+}_{s}x\right){<}_s\left(z{+}_{s}x\right)\right)\right)\right)$$
	addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
	addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
	addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
	addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
	addsproplem5.6	$$⊢\phi \to \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)$$
Assertion	addsproplem5	$$⊢\phi \to \left(Y{+}_{s}X\right){<}_s\left(Z{+}_{s}X\right)$$

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	$$⊢\phi \to \forall x\in \mathrm{No}\forall y\in \mathrm{No}\forall z\in \mathrm{No}\left(\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\right)\cup \left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left(z\right)\right)\in \left(\left(\mathrm{bday}\left(X\right)+\mathrm{bday}\left(Y\right)\right)\cup \left(\mathrm{bday}\left(X\right)+\mathrm{bday}\left(Z\right)\right)\right)\to \left(x{+}_{s}y\in \mathrm{No}\wedge \left(y{<}_{s}z\to \left(y{+}_{s}x\right){<}_s\left(z{+}_{s}x\right)\right)\right)\right)$$
2		addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
3		addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
4		addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
5		addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
6		addsproplem5.6	$$⊢\phi \to \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)$$
7	1 2 3	addsproplem3	$$⊢\phi \to \left(X{+}_{s}Y\in \mathrm{No}\wedge \left(\left\{e|\exists f\in L\left(X\right)e=f{+}_{s}Y\right\}\cup \left\{g|\exists h\in L\left(Y\right)g=X{+}_{s}h\right\}\right){\ll }_s\left\{X{+}_{s}Y\right\}\wedge \left\{X{+}_{s}Y\right\}{\ll }_s\left(\left\{a|\exists c\in R\left(X\right)a=c{+}_{s}Y\right\}\cup \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\right)\right)$$
8	7	simp3d	$$⊢\phi \to \left\{X{+}_{s}Y\right\}{\ll }_s\left(\left\{a|\exists c\in R\left(X\right)a=c{+}_{s}Y\right\}\cup \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\right)$$
9		ovex	$$⊢X{+}_{s}Y\in \mathrm{V}$$
10	9	snid	$$⊢X{+}_{s}Y\in \left\{X{+}_{s}Y\right\}$$
11	10	a1i	$$⊢\phi \to X{+}_{s}Y\in \left\{X{+}_{s}Y\right\}$$
12		bdayon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
13		oldbday	$$⊢\left(\mathrm{bday}\left(Y\right)\in \mathrm{On}\wedge Z\in \mathrm{No}\right)\to \left(Z\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)$$
14	12 4 13	sylancr	$$⊢\phi \to \left(Z\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\leftrightarrow \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)$$
15	6 14	mpbird	$$⊢\phi \to Z\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)$$
16		elright	$$⊢Z\in R\left(Y\right)\leftrightarrow \left(Z\in \mathrm{Old}\left(\mathrm{bday}\left(Y\right)\right)\wedge Y{<}_{s}Z\right)$$
17	15 5 16	sylanbrc	$$⊢\phi \to Z\in R\left(Y\right)$$
18		eqid	$$⊢X{+}_{s}Z=X{+}_{s}Z$$
19		oveq2	$$⊢d=Z\to X{+}_{s}d=X{+}_{s}Z$$
20	19	rspceeqv	$$⊢\left(Z\in R\left(Y\right)\wedge X{+}_{s}Z=X{+}_{s}Z\right)\to \exists d\in R\left(Y\right)X{+}_{s}Z=X{+}_{s}d$$
21	17 18 20	sylancl	$$⊢\phi \to \exists d\in R\left(Y\right)X{+}_{s}Z=X{+}_{s}d$$
22		ovex	$$⊢X{+}_{s}Z\in \mathrm{V}$$
23		eqeq1	$$⊢b=X{+}_{s}Z\to \left(b=X{+}_{s}d\leftrightarrow X{+}_{s}Z=X{+}_{s}d\right)$$
24	23	rexbidv	$$⊢b=X{+}_{s}Z\to \left(\exists d\in R\left(Y\right)b=X{+}_{s}d\leftrightarrow \exists d\in R\left(Y\right)X{+}_{s}Z=X{+}_{s}d\right)$$
25	22 24	elab	$$⊢X{+}_{s}Z\in \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\leftrightarrow \exists d\in R\left(Y\right)X{+}_{s}Z=X{+}_{s}d$$
26	21 25	sylibr	$$⊢\phi \to X{+}_{s}Z\in \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}$$
27		elun2	$$⊢X{+}_{s}Z\in \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\to X{+}_{s}Z\in \left(\left\{a|\exists c\in R\left(X\right)a=c{+}_{s}Y\right\}\cup \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\right)$$
28	26 27	syl	$$⊢\phi \to X{+}_{s}Z\in \left(\left\{a|\exists c\in R\left(X\right)a=c{+}_{s}Y\right\}\cup \left\{b|\exists d\in R\left(Y\right)b=X{+}_{s}d\right\}\right)$$
29	8 11 28	sltssepcd	$$⊢\phi \to \left(X{+}_{s}Y\right){<}_s\left(X{+}_{s}Z\right)$$
30	3 2	addscomd	$$⊢\phi \to Y{+}_{s}X=X{+}_{s}Y$$
31	4 2	addscomd	$$⊢\phi \to Z{+}_{s}X=X{+}_{s}Z$$
32	29 30 31	3brtr4d	$$⊢\phi \to \left(Y{+}_{s}X\right){<}_s\left(Z{+}_{s}X\right)$$