Theorem dmuz

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

	Ref	Expression
Assertion	dmuz	$$⊢\mathrm{dom}{\mathbb{Z}}_{\ge }=\mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		uzf	$$⊢{\mathbb{Z}}_{\ge }:\mathbb{Z}⟶𝒫\mathbb{Z}$$
2	1	fdmi	$$⊢\mathrm{dom}{\mathbb{Z}}_{\ge }=\mathbb{Z}$$