Theorem ltwenn0

Description: "Less than" is a well-order on the nonnegative integers. (Contributed by Thierry Arnoux, 29-Oct-2026)

	Ref	Expression
Assertion	ltwenn0	⊢ < We ℕ0

Proof

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