Metamath Proof Explorer

Theorem ltwefz

Description: Less than well-orders a set of finite integers. (Contributed by Scott Fenton, 8-Aug-2013)

Ref Expression
Assertion ltwefz 
|- < We ( M ... N )

Proof

Step Hyp Ref Expression
1 fzssuz 
 |-  ( M ... N ) C_ ( ZZ>= ` M )
2 ltweuz 
 |-  < We ( ZZ>= ` M )
3 wess 
 |-  ( ( M ... N ) C_ ( ZZ>= ` M ) -> ( < We ( ZZ>= ` M ) -> < We ( M ... N ) ) )
4 1 2 3 mp2 
 |-  < We ( M ... N )