Theorem ltsp1d

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

	Ref	Expression
Hypothesis	ltsp1d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
Assertion	ltsp1d	⊢ ( 𝜑 → 𝐴 <s ( 𝐴 +s 1s ) )

Proof

Step	Hyp	Ref	Expression
1		ltsp1d.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2	1	addsridd	⊢ ( 𝜑 → ( 𝐴 +s 0s ) = 𝐴 )
3		0lt1s	⊢ 0s <s 1s
4		0no	⊢ 0s ∈ No
5	4	a1i	⊢ ( 𝜑 → 0s ∈ No )
6		1no	⊢ 1s ∈ No
7	6	a1i	⊢ ( 𝜑 → 1s ∈ No )
8	5 7 1	ltadds2d	⊢ ( 𝜑 → ( 0s <s 1s ↔ ( 𝐴 +s 0s ) <s ( 𝐴 +s 1s ) ) )
9	3 8	mpbii	⊢ ( 𝜑 → ( 𝐴 +s 0s ) <s ( 𝐴 +s 1s ) )
10	2 9	eqbrtrrd	⊢ ( 𝜑 → 𝐴 <s ( 𝐴 +s 1s ) )