Theorem slt2addd

Description: Adding both sides of two surreal less-than relations. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Hypotheses	slt2addd.1	$$⊢\phi \to A\in \mathrm{No}$$
	slt2addd.2	$$⊢\phi \to B\in \mathrm{No}$$
	slt2addd.3	$$⊢\phi \to C\in \mathrm{No}$$
	slt2addd.4	$$⊢\phi \to D\in \mathrm{No}$$
	slt2addd.5	$$⊢\phi \to A{<}_{s}C$$
	slt2addd.6	$$⊢\phi \to B{<}_{s}D$$
Assertion	slt2addd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		slt2addd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		slt2addd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		slt2addd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		slt2addd.4	$$⊢\phi \to D\in \mathrm{No}$$
5		slt2addd.5	$$⊢\phi \to A{<}_{s}C$$
6		slt2addd.6	$$⊢\phi \to B{<}_{s}D$$
7	1 2	addscld	$$⊢\phi \to A{+}_{s}B\in \mathrm{No}$$
8	3 2	addscld	$$⊢\phi \to C{+}_{s}B\in \mathrm{No}$$
9	3 4	addscld	$$⊢\phi \to C{+}_{s}D\in \mathrm{No}$$
10	1 3 2	sltadd1d	$$⊢\phi \to \left(A{<}_{s}C\leftrightarrow \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}B\right)\right)$$
11	5 10	mpbid	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}B\right)$$
12	2 4 3	sltadd2d	$$⊢\phi \to \left(B{<}_{s}D\leftrightarrow \left(C{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)\right)$$
13	6 12	mpbid	$$⊢\phi \to \left(C{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)$$
14	7 8 9 11 13	slttrd	$$⊢\phi \to \left(A{+}_{s}B\right){<}_s\left(C{+}_{s}D\right)$$