Metamath Proof Explorer

Theorem addsproplem3

Description: Lemma for surreal addition properties. Show the cut properties of surreal addition. (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))))$
		addsproplem2.2	$⊢ φ \to X \in No$
		addsproplem2.3	$⊢ φ \to Y \in No$
	Assertion	addsproplem3	$⊢ φ \to (X +_{s} Y \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$

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		addsproplem2.2	$⊢ φ \to X \in No$
3		addsproplem2.3	$⊢ φ \to Y \in No$
4	1 2 3	addsproplem2	$⊢ φ \to (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$
5		cutcuts	$⊢ (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \to ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} \land \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$
6	4 5	syl	$⊢ φ \to ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} \land \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$
7		addsval2	$⊢ (X \in No \land Y \in No) \to X +_{s} Y = (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$
8	2 3 7	syl2anc	$⊢ φ \to X +_{s} Y = (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})$
9	8	eleq1d	$⊢ φ \to (X +_{s} Y \in No \leftrightarrow (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \in No)$
10	8	sneqd	$⊢ φ \to \{X +_{s} Y\} = \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\}$
11	10	breq2d	$⊢ φ \to ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \leftrightarrow (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\})$
12	10	breq1d	$⊢ φ \to (\{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \leftrightarrow \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$
13	9 11 12	3anbi123d	$⊢ φ \to ((X +_{s} Y \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})) \leftrightarrow ((\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}) \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} \land \{(\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) \|_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\})))$
14	6 13	mpbird	$⊢ φ \to (X +_{s} Y \in No \land (\{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\}))$