Metamath Proof Explorer

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 ⊢ J = TopOpen ⁡ ℂ fld
Assertion sszcld ⊢ A ⊆ ℤ → A ∈ Clsd ⁡ J

Proof

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