Theorem ltsp1d

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

	Ref	Expression
Hypothesis	ltsp1d.1	|- ( ph -> A e. No )
Assertion	ltsp1d	|- ( ph -> A

Proof

Step	Hyp	Ref	Expression
1		ltsp1d.1	|- ( ph -> A e. No )
2	1	addsridd	|- ( ph -> ( A +s 0s ) = A )
3		0lt1s	|- 0s
4		0no	|- 0s e. No
5	4	a1i	|- ( ph -> 0s e. No )
6		1no	|- 1s e. No
7	6	a1i	|- ( ph -> 1s e. No )
8	5 7 1	ltadds2d	|- ( ph -> ( 0s ( A +s 0s )
9	3 8	mpbii	|- ( ph -> ( A +s 0s )
10	2 9	eqbrtrrd	|- ( ph -> A