Theorem ltwenn

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

	Ref	Expression
Assertion	ltwenn	$$⊢<\mathrm{We}\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		ltweuz	$$⊢<\mathrm{We}{\mathbb{Z}}_{\ge 1}$$
2		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
3		weeq2	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}\to \left(<\mathrm{We}\mathbb{N}\leftrightarrow <\mathrm{We}{\mathbb{Z}}_{\ge 1}\right)$$
4	2 3	ax-mp	$$⊢<\mathrm{We}\mathbb{N}\leftrightarrow <\mathrm{We}{\mathbb{Z}}_{\ge 1}$$
5	1 4	mpbir	$$⊢<\mathrm{We}\mathbb{N}$$