sszcld

Description: Every subset of the integers are closed in the topology on CC . (Contributed by Mario Carneiro, 6-Jul-2017)

		Ref	Expression
	Hypothesis	recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	sszcld	$⊢ A \subseteq ℤ \to A \in Clsd (J)$

Step	Hyp	Ref	Expression
1		recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
2	1	zcld2	$⊢ ℤ \in Clsd (J)$
3		id	$⊢ A \subseteq ℤ \to A \subseteq ℤ$
4		zex	$⊢ ℤ \in V$
5		difss	$⊢ ℤ ∖ A \subseteq ℤ$
6	4 5	elpwi2	$⊢ ℤ ∖ A \in 𝒫 ℤ$
7	1	zdis	$⊢ J ↾_{𝑡} ℤ = 𝒫 ℤ$
8	6 7	eleqtrri	$⊢ ℤ ∖ A \in (J ↾_{𝑡} ℤ)$
9	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
10		zsscn	$⊢ ℤ \subseteq ℂ$
11		resttopon	$⊢ (J \in TopOn (ℂ) \land ℤ \subseteq ℂ) \to J ↾_{𝑡} ℤ \in TopOn (ℤ)$
12	9 10 11	mp2an	$⊢ J ↾_{𝑡} ℤ \in TopOn (ℤ)$
13	12	topontopi	$⊢ J ↾_{𝑡} ℤ \in Top$
14	12	toponunii	$⊢ ℤ = ⋃ (J ↾_{𝑡} ℤ)$
15	14	iscld	$⊢ J ↾_{𝑡} ℤ \in Top \to (A \in Clsd (J ↾_{𝑡} ℤ) \leftrightarrow (A \subseteq ℤ \land ℤ ∖ A \in (J ↾_{𝑡} ℤ)))$
16	13 15	ax-mp	$⊢ A \in Clsd (J ↾_{𝑡} ℤ) \leftrightarrow (A \subseteq ℤ \land ℤ ∖ A \in (J ↾_{𝑡} ℤ))$
17	3 8 16	sylanblrc	$⊢ A \subseteq ℤ \to A \in Clsd (J ↾_{𝑡} ℤ)$
18		restcldr	$⊢ (ℤ \in Clsd (J) \land A \in Clsd (J ↾_{𝑡} ℤ)) \to A \in Clsd (J)$
19	2 17 18	sylancr	$⊢ A \subseteq ℤ \to A \in Clsd (J)$

Metamath Proof Explorer