Theorem ltwenn

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

	Ref	Expression
Assertion	ltwenn	⊢ < We ℕ

Proof

Step	Hyp	Ref	Expression
1		ltweuz	⊢ < We ( ℤ≥ ‘ 1 )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3		weeq2	⊢ ( ℕ = ( ℤ≥ ‘ 1 ) → ( < We ℕ ↔ < We ( ℤ≥ ‘ 1 ) ) )
4	2 3	ax-mp	⊢ ( < We ℕ ↔ < We ( ℤ≥ ‘ 1 ) )
5	1 4	mpbir	⊢ < We ℕ