Theorem 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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	sszcld	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		recld2.1	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2	1	zcld2	⊢ ℤ ∈ ( Clsd ‘ 𝐽 )
3		id	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ⊆ ℤ )
4		zex	⊢ ℤ ∈ V
5		difss	⊢ ( ℤ ∖ 𝐴 ) ⊆ ℤ
6	4 5	elpwi2	⊢ ( ℤ ∖ 𝐴 ) ∈ 𝒫 ℤ
7	1	zdis	⊢ ( 𝐽 ↾t ℤ ) = 𝒫 ℤ
8	6 7	eleqtrri	⊢ ( ℤ ∖ 𝐴 ) ∈ ( 𝐽 ↾t ℤ )
9	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
10		zsscn	⊢ ℤ ⊆ ℂ
11		resttopon	⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ℤ ⊆ ℂ ) → ( 𝐽 ↾t ℤ ) ∈ ( TopOn ‘ ℤ ) )
12	9 10 11	mp2an	⊢ ( 𝐽 ↾t ℤ ) ∈ ( TopOn ‘ ℤ )
13	12	topontopi	⊢ ( 𝐽 ↾t ℤ ) ∈ Top
14	12	toponunii	⊢ ℤ = ∪ ( 𝐽 ↾t ℤ )
15	14	iscld	⊢ ( ( 𝐽 ↾t ℤ ) ∈ Top → ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 ↾t ℤ ) ) ↔ ( 𝐴 ⊆ ℤ ∧ ( ℤ ∖ 𝐴 ) ∈ ( 𝐽 ↾t ℤ ) ) ) )
16	13 15	ax-mp	⊢ ( 𝐴 ∈ ( Clsd ‘ ( 𝐽 ↾t ℤ ) ) ↔ ( 𝐴 ⊆ ℤ ∧ ( ℤ ∖ 𝐴 ) ∈ ( 𝐽 ↾t ℤ ) ) )
17	3 8 16	sylanblrc	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ∈ ( Clsd ‘ ( 𝐽 ↾t ℤ ) ) )
18		restcldr	⊢ ( ( ℤ ∈ ( Clsd ‘ 𝐽 ) ∧ 𝐴 ∈ ( Clsd ‘ ( 𝐽 ↾t ℤ ) ) ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
19	2 17 18	sylancr	⊢ ( 𝐴 ⊆ ℤ → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )