Metamath Proof Explorer

Theorem n0sleltp1

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

Ref Expression
Assertion n0sleltp1 
|- ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> M

Proof

Step Hyp Ref Expression
1 n0sno 
 |-  ( M e. NN0_s -> M e. No )
2 1 adantr 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> M e. No )
3 n0sno 
 |-  ( N e. NN0_s -> N e. No )
4 3 adantl 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> N e. No )
5 1sno 
 |-  1s e. No
6 5 a1i 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> 1s e. No )
7 2 4 6 sleadd1d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> ( M +s 1s ) <_s ( N +s 1s ) ) )
8 peano2n0s 
 |-  ( N e. NN0_s -> ( N +s 1s ) e. NN0_s )
9 n0sltp1le 
 |-  ( ( M e. NN0_s /\ ( N +s 1s ) e. NN0_s ) -> ( M  ( M +s 1s ) <_s ( N +s 1s ) ) )
10 8 9 sylan2 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M  ( M +s 1s ) <_s ( N +s 1s ) ) )
11 7 10 bitr4d 
 |-  ( ( M e. NN0_s /\ N e. NN0_s ) -> ( M <_s N <-> M