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

Proof

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

Metamath Proof Explorer

Theorem addsproplem5

Proof