Metamath Proof Explorer

Theorem ltwenn

Description: Less than well-orders the naturals. (Contributed by Scott Fenton, 6-Aug-2013)

Ref Expression
Assertion ltwenn 
|- < We NN

Proof

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