Theorem dmuz

Description: Domain of the upper integers function. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Assertion	dmuz	⊢ dom ℤ≥ = ℤ

Proof

Step	Hyp	Ref	Expression
1		uzf	⊢ ℤ≥ : ℤ ⟶ 𝒫 ℤ
2	1	fdmi	⊢ dom ℤ≥ = ℤ