Theorem n0lesltp1

Description: Non-negative surreal ordering relation. (Contributed by Scott Fenton, 7-Nov-2025)

	Ref	Expression
Assertion	n0lesltp1	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ 𝑀 <s ( 𝑁 +s 1s ) ) )

Proof

Step	Hyp	Ref	Expression
1		n0no	⊢ ( 𝑀 ∈ ℕ0s → 𝑀 ∈ No )
2	1	adantr	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑀 ∈ No )
3		n0no	⊢ ( 𝑁 ∈ ℕ0s → 𝑁 ∈ No )
4	3	adantl	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 𝑁 ∈ No )
5		1no	⊢ 1s ∈ No
6	5	a1i	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → 1s ∈ No )
7	2 4 6	leadds1d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ ( 𝑀 +s 1s ) ≤s ( 𝑁 +s 1s ) ) )
8		peano2n0s	⊢ ( 𝑁 ∈ ℕ0s → ( 𝑁 +s 1s ) ∈ ℕ0s )
9		n0ltsp1le	⊢ ( ( 𝑀 ∈ ℕ0s ∧ ( 𝑁 +s 1s ) ∈ ℕ0s ) → ( 𝑀 <s ( 𝑁 +s 1s ) ↔ ( 𝑀 +s 1s ) ≤s ( 𝑁 +s 1s ) ) )
10	8 9	sylan2	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 <s ( 𝑁 +s 1s ) ↔ ( 𝑀 +s 1s ) ≤s ( 𝑁 +s 1s ) ) )
11	7 10	bitr4d	⊢ ( ( 𝑀 ∈ ℕ0s ∧ 𝑁 ∈ ℕ0s ) → ( 𝑀 ≤s 𝑁 ↔ 𝑀 <s ( 𝑁 +s 1s ) ) )