Theorem ltwefz

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

	Ref	Expression
Assertion	ltwefz	⊢ < We ( 𝑀 ... 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		fzssuz	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 )
2		ltweuz	⊢ < We ( ℤ≥ ‘ 𝑀 )
3		wess	⊢ ( ( 𝑀 ... 𝑁 ) ⊆ ( ℤ≥ ‘ 𝑀 ) → ( < We ( ℤ≥ ‘ 𝑀 ) → < We ( 𝑀 ... 𝑁 ) ) )
4	1 2 3	mp2	⊢ < We ( 𝑀 ... 𝑁 )