Theorem zcld2

Description: The integers are a closed set in the topology on CC . (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Hypothesis	recld2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	zcld2	$$⊢\mathbb{Z}\in \mathrm{Clsd}\left(J\right)$$

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	recld2	$$⊢ℝ\in \mathrm{Clsd}\left(J\right)$$
3	1	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=J{\upharpoonright }_{𝑡}ℝ$$
4	3	eqcomi	$$⊢J{\upharpoonright }_{𝑡}ℝ=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
5	4	zcld	$$⊢\mathbb{Z}\in \mathrm{Clsd}\left(J{\upharpoonright }_{𝑡}ℝ\right)$$
6		restcldr	$$⊢\left(ℝ\in \mathrm{Clsd}\left(J\right)\wedge \mathbb{Z}\in \mathrm{Clsd}\left(J{\upharpoonright }_{𝑡}ℝ\right)\right)\to \mathbb{Z}\in \mathrm{Clsd}\left(J\right)$$
7	2 5 6	mp2an	$$⊢\mathbb{Z}\in \mathrm{Clsd}\left(J\right)$$