This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( 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 ‘ 𝐽 ) )