Theorem ltsp1d

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

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

Proof

Step	Hyp	Ref	Expression
1		ltsp1d.1	$$⊢\phi \to A\in \mathrm{No}$$
2	1	addsridd	$$⊢\phi \to A{+}_s{0}_s=A$$
3		0lt1s	$$⊢0_s{<}_s{1}_s$$
4		0no	$$⊢0_s\in \mathrm{No}$$
5	4	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
6		1no	$$⊢1_s\in \mathrm{No}$$
7	6	a1i	$$⊢\phi \to 1_s\in \mathrm{No}$$
8	5 7 1	ltadds2d	$$⊢\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)$$