This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltwenn

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

		Ref	Expression
	Assertion	ltwenn	$⊢ < We ℕ$

Step	Hyp	Ref	Expression
1		ltweuz	$⊢ < We ℤ_{\geq 1}$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		weeq2	$⊢ ℕ = ℤ_{\geq 1} \to (< We ℕ \leftrightarrow < We ℤ_{\geq 1})$
4	2 3	ax-mp	$⊢ < We ℕ \leftrightarrow < We ℤ_{\geq 1}$
5	1 4	mpbir	$⊢ < We ℕ$