Theorem sltp1d

Description: A surreal is less than itself plus one. (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypothesis	sltp1d.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	sltp1d	$$⊢\phi \to A{<}_s\left(A{+}_s{1}_s\right)$$

Proof

Step	Hyp	Ref	Expression
1		sltp1d.1	$$⊢\phi \to A\in \mathrm{No}$$
2	1	addsridd	$$⊢\phi \to A{+}_s{0}_s=A$$
3		0slt1s	$$⊢0_s{<}_s{1}_s$$
4		0sno	$$⊢0_s\in \mathrm{No}$$
5	4	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
6		1sno	$$⊢1_s\in \mathrm{No}$$
7	6	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
8	5 7 1	sltadd2d	$$⊢\phi \to \left(0_s{<}_s{1}_s\leftrightarrow \left(A{+}_s{0}_s\right){<}_s\left(A{+}_s{1}_s\right)\right)$$
9	3 8	mpbii	$$⊢\phi \to \left(A{+}_s{0}_s\right){<}_s\left(A{+}_s{1}_s\right)$$
10	2 9	eqbrtrrd	$$⊢\phi \to A{<}_s\left(A{+}_s{1}_s\right)$$