Theorem sltp1d

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

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

Proof

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