Theorem ltwefz

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

	Ref	Expression
Assertion	ltwefz	$$⊢<\mathrm{We}\left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		fzssuz	$$⊢\left(M\dots N\right)\subseteq {\mathbb{Z}}_{\ge M}$$
2		ltweuz	$$⊢<\mathrm{We}{\mathbb{Z}}_{\ge M}$$
3		wess	$$⊢\left(M\dots N\right)\subseteq {\mathbb{Z}}_{\ge M}\to \left(<\mathrm{We}{\mathbb{Z}}_{\ge M}\to <\mathrm{We}\left(M\dots N\right)\right)$$
4	1 2 3	mp2	$$⊢<\mathrm{We}\left(M\dots N\right)$$