Theorem nn0uz

Description: Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005)

	Ref	Expression
Assertion	nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )

Proof

Step	Hyp	Ref	Expression
1		nn0zrab	⊢ ℕ0 = { 𝑘 ∈ ℤ ∣ 0 ≤ 𝑘 }
2		0z	⊢ 0 ∈ ℤ
3		uzval	⊢ ( 0 ∈ ℤ → ( ℤ≥ ‘ 0 ) = { 𝑘 ∈ ℤ ∣ 0 ≤ 𝑘 } )
4	2 3	ax-mp	⊢ ( ℤ≥ ‘ 0 ) = { 𝑘 ∈ ℤ ∣ 0 ≤ 𝑘 }
5	1 4	eqtr4i	⊢ ℕ0 = ( ℤ≥ ‘ 0 )