addscut

Description: Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addscut.1	$⊢ φ \to X \in No$
	addscut.2	$⊢ φ \to Y \in No$
Assertion	addscut	$⊢ φ \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		addscut.1	$⊢ φ \to X \in No$
2		addscut.2	$⊢ φ \to Y \in No$
3	1 2	addscutlem	$⊢ φ \to (X +_{s} Y \in No \land (\{a \| \exists b \in L (X) a = b +_{s} Y\} \cup \{c \| \exists d \in L (Y) c = X +_{s} d\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{e \| \exists f \in R (X) e = f +_{s} Y\} \cup \{g \| \exists h \in R (Y) g = X +_{s} h\}))$
4		biid	$⊢ X +_{s} Y \in No \leftrightarrow X +_{s} Y \in No$
5		oveq1	$⊢ l = b \to l +_{s} Y = b +_{s} Y$
6	5	eqeq2d	$⊢ l = b \to (p = l +_{s} Y \leftrightarrow p = b +_{s} Y)$
7	6	cbvrexvw	$⊢ \exists l \in L (X) p = l +_{s} Y \leftrightarrow \exists b \in L (X) p = b +_{s} Y$
8		eqeq1	$⊢ p = a \to (p = b +_{s} Y \leftrightarrow a = b +_{s} Y)$
9	8	rexbidv	$⊢ p = a \to (\exists b \in L (X) p = b +_{s} Y \leftrightarrow \exists b \in L (X) a = b +_{s} Y)$
10	7 9	bitrid	$⊢ p = a \to (\exists l \in L (X) p = l +_{s} Y \leftrightarrow \exists b \in L (X) a = b +_{s} Y)$
11	10	cbvabv	$⊢ \{p \| \exists l \in L (X) p = l +_{s} Y\} = \{a \| \exists b \in L (X) a = b +_{s} Y\}$
12		oveq2	$⊢ m = d \to X +_{s} m = X +_{s} d$
13	12	eqeq2d	$⊢ m = d \to (q = X +_{s} m \leftrightarrow q = X +_{s} d)$
14	13	cbvrexvw	$⊢ \exists m \in L (Y) q = X +_{s} m \leftrightarrow \exists d \in L (Y) q = X +_{s} d$
15		eqeq1	$⊢ q = c \to (q = X +_{s} d \leftrightarrow c = X +_{s} d)$
16	15	rexbidv	$⊢ q = c \to (\exists d \in L (Y) q = X +_{s} d \leftrightarrow \exists d \in L (Y) c = X +_{s} d)$
17	14 16	bitrid	$⊢ q = c \to (\exists m \in L (Y) q = X +_{s} m \leftrightarrow \exists d \in L (Y) c = X +_{s} d)$
18	17	cbvabv	$⊢ \{q \| \exists m \in L (Y) q = X +_{s} m\} = \{c \| \exists d \in L (Y) c = X +_{s} d\}$
19	11 18	uneq12i	$⊢ \{p \| \exists l \in L (X) p = l +_{s} Y\} \cup \{q \| \exists m \in L (Y) q = X +_{s} m\} = \{a \| \exists b \in L (X) a = b +_{s} Y\} \cup \{c \| \exists d \in L (Y) c = X +_{s} d\}$
20	19	breq1i	$⊢ (\{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 (\{a \| \exists b \in L (X) a = b +_{s} Y\} \cup \{c \| \exists d \in L (Y) c = X +_{s} d\}) ≪_{s} \{X +_{s} Y\}$
21		oveq1	$⊢ r = f \to r +_{s} Y = f +_{s} Y$
22	21	eqeq2d	$⊢ r = f \to (w = r +_{s} Y \leftrightarrow w = f +_{s} Y)$
23	22	cbvrexvw	$⊢ \exists r \in R (X) w = r +_{s} Y \leftrightarrow \exists f \in R (X) w = f +_{s} Y$
24		eqeq1	$⊢ w = e \to (w = f +_{s} Y \leftrightarrow e = f +_{s} Y)$
25	24	rexbidv	$⊢ w = e \to (\exists f \in R (X) w = f +_{s} Y \leftrightarrow \exists f \in R (X) e = f +_{s} Y)$
26	23 25	bitrid	$⊢ w = e \to (\exists r \in R (X) w = r +_{s} Y \leftrightarrow \exists f \in R (X) e = f +_{s} Y)$
27	26	cbvabv	$⊢ \{w \| \exists r \in R (X) w = r +_{s} Y\} = \{e \| \exists f \in R (X) e = f +_{s} Y\}$
28		oveq2	$⊢ s = h \to X +_{s} s = X +_{s} h$
29	28	eqeq2d	$⊢ s = h \to (t = X +_{s} s \leftrightarrow t = X +_{s} h)$
30	29	cbvrexvw	$⊢ \exists s \in R (Y) t = X +_{s} s \leftrightarrow \exists h \in R (Y) t = X +_{s} h$
31		eqeq1	$⊢ t = g \to (t = X +_{s} h \leftrightarrow g = X +_{s} h)$
32	31	rexbidv	$⊢ t = g \to (\exists h \in R (Y) t = X +_{s} h \leftrightarrow \exists h \in R (Y) g = X +_{s} h)$
33	30 32	bitrid	$⊢ t = g \to (\exists s \in R (Y) t = X +_{s} s \leftrightarrow \exists h \in R (Y) g = X +_{s} h)$
34	33	cbvabv	$⊢ \{t \| \exists s \in R (Y) t = X +_{s} s\} = \{g \| \exists h \in R (Y) g = X +_{s} h\}$
35	27 34	uneq12i	$⊢ \{w \| \exists r \in R (X) w = r +_{s} Y\} \cup \{t \| \exists s \in R (Y) t = X +_{s} s\} = \{e \| \exists f \in R (X) e = f +_{s} Y\} \cup \{g \| \exists h \in R (Y) g = X +_{s} h\}$
36	35	breq2i	$⊢ \{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 \{X +_{s} Y\} ≪_{s} (\{e \| \exists f \in R (X) e = f +_{s} Y\} \cup \{g \| \exists h \in R (Y) g = X +_{s} h\})$
37	4 20 36	3anbi123i	$⊢ (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 (X +_{s} Y \in No \land (\{a \| \exists b \in L (X) a = b +_{s} Y\} \cup \{c \| \exists d \in L (Y) c = X +_{s} d\}) ≪_{s} \{X +_{s} Y\} \land \{X +_{s} Y\} ≪_{s} (\{e \| \exists f \in R (X) e = f +_{s} Y\} \cup \{g \| \exists h \in R (Y) g = X +_{s} h\}))$
38	3 37	sylibr	$⊢ φ \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\}))$

Metamath Proof Explorer

Theorem addscut

Proof