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 ` CCfld )
Assertion sszcld 
|- ( A C_ ZZ -> A e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 recld2.1 
 |-  J = ( TopOpen ` CCfld )
2 1 zcld2 
 |-  ZZ e. ( Clsd ` J )
3 id 
 |-  ( A C_ ZZ -> A C_ ZZ )
4 zex 
 |-  ZZ e. _V
5 difss 
 |-  ( ZZ \ A ) C_ ZZ
6 4 5 elpwi2 
 |-  ( ZZ \ A ) e. ~P ZZ
7 1 zdis 
 |-  ( J |`t ZZ ) = ~P ZZ
8 6 7 eleqtrri 
 |-  ( ZZ \ A ) e. ( J |`t ZZ )
9 1 cnfldtopon 
 |-  J e. ( TopOn ` CC )
10 zsscn 
 |-  ZZ C_ CC
11 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ ZZ C_ CC ) -> ( J |`t ZZ ) e. ( TopOn ` ZZ ) )
12 9 10 11 mp2an 
 |-  ( J |`t ZZ ) e. ( TopOn ` ZZ )
13 12 topontopi 
 |-  ( J |`t ZZ ) e. Top
14 12 toponunii 
 |-  ZZ = U. ( J |`t ZZ )
15 14 iscld 
 |-  ( ( J |`t ZZ ) e. Top -> ( A e. ( Clsd ` ( J |`t ZZ ) ) <-> ( A C_ ZZ /\ ( ZZ \ A ) e. ( J |`t ZZ ) ) ) )
16 13 15 ax-mp 
 |-  ( A e. ( Clsd ` ( J |`t ZZ ) ) <-> ( A C_ ZZ /\ ( ZZ \ A ) e. ( J |`t ZZ ) ) )
17 3 8 16 sylanblrc 
 |-  ( A C_ ZZ -> A e. ( Clsd ` ( J |`t ZZ ) ) )
18 restcldr 
 |-  ( ( ZZ e. ( Clsd ` J ) /\ A e. ( Clsd ` ( J |`t ZZ ) ) ) -> A e. ( Clsd ` J ) )
19 2 17 18 sylancr 
 |-  ( A C_ ZZ -> A e. ( Clsd ` J ) )