Metamath Proof Explorer

Theorem ltwenn0

Description: "Less than" is a well-order on the nonnegative integers. (Contributed by Thierry Arnoux, 29-Oct-2026)

Ref Expression
Assertion ltwenn0 
|- < We NN0

Proof

Step Hyp Ref Expression
1 ltweuz 
 |-  < We ( ZZ>= ` 0 )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 weeq2 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> ( < We NN0 <-> < We ( ZZ>= ` 0 ) ) )
4 2 3 ax-mp 
 |-  ( < We NN0 <-> < We ( ZZ>= ` 0 ) )
5 1 4 mpbir 
 |-  < We NN0