zdis

Description: The integers are a discrete set in the topology on CC . (Contributed by Mario Carneiro, 19-Sep-2015)

		Ref	Expression
	Hypothesis	recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
	Assertion	zdis	$⊢ J ↾_{𝑡} ℤ = 𝒫 ℤ$

Proof

Step	Hyp	Ref	Expression
1		recld2.1	$⊢ J = TopOpen (ℂ_{fld})$
2		restsspw	$⊢ J ↾_{𝑡} ℤ \subseteq 𝒫 ℤ$
3		elpwi	$⊢ x \in 𝒫 ℤ \to x \subseteq ℤ$
4	3	sselda	$⊢ (x \in 𝒫 ℤ \land y \in x) \to y \in ℤ$
5	4	zcnd	$⊢ (x \in 𝒫 ℤ \land y \in x) \to y \in ℂ$
6		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
7		1xr	$⊢ 1 \in ℝ^{*}$
8	1	cnfldtopn	$⊢ J = MetOpen (abs \circ -)$
9	8	blopn	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land 1 \in ℝ^{*}) \to y ball (abs \circ -) 1 \in J$
10	6 7 9	mp3an13	$⊢ y \in ℂ \to y ball (abs \circ -) 1 \in J$
11	1	cnfldtop	$⊢ J \in Top$
12		zex	$⊢ ℤ \in V$
13		elrestr	$⊢ (J \in Top \land ℤ \in V \land y ball (abs \circ -) 1 \in J) \to (y ball (abs \circ -) 1) \cap ℤ \in (J ↾_{𝑡} ℤ)$
14	11 12 13	mp3an12	$⊢ y ball (abs \circ -) 1 \in J \to (y ball (abs \circ -) 1) \cap ℤ \in (J ↾_{𝑡} ℤ)$
15	5 10 14	3syl	$⊢ (x \in 𝒫 ℤ \land y \in x) \to (y ball (abs \circ -) 1) \cap ℤ \in (J ↾_{𝑡} ℤ)$
16		1rp	$⊢ 1 \in ℝ^{+}$
17		blcntr	$⊢ (abs \circ - \in ∞Met (ℂ) \land y \in ℂ \land 1 \in ℝ^{+}) \to y \in (y ball (abs \circ -) 1)$
18	6 16 17	mp3an13	$⊢ y \in ℂ \to y \in (y ball (abs \circ -) 1)$
19	5 18	syl	$⊢ (x \in 𝒫 ℤ \land y \in x) \to y \in (y ball (abs \circ -) 1)$
20	19 4	elind	$⊢ (x \in 𝒫 ℤ \land y \in x) \to y \in ((y ball (abs \circ -) 1) \cap ℤ)$
21	5	adantr	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y \in ℂ$
22		simpr	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to z \in ((y ball (abs \circ -) 1) \cap ℤ)$
23	22	elin2d	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to z \in ℤ$
24	23	zcnd	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to z \in ℂ$
25	4	adantr	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y \in ℤ$
26	25 23	zsubcld	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y - z \in ℤ$
27	26	zcnd	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y - z \in ℂ$
28		eqid	$⊢ abs \circ - = abs \circ -$
29	28	cnmetdval	$⊢ (y \in ℂ \land z \in ℂ) \to y (abs \circ -) z = \|y - z\|$
30	21 24 29	syl2anc	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y (abs \circ -) z = \|y - z\|$
31	22	elin1d	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to z \in (y ball (abs \circ -) 1)$
32		elbl2	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (y \in ℂ \land z \in ℂ)) \to (z \in (y ball (abs \circ -) 1) \leftrightarrow y (abs \circ -) z < 1)$
33	6 7 32	mpanl12	$⊢ (y \in ℂ \land z \in ℂ) \to (z \in (y ball (abs \circ -) 1) \leftrightarrow y (abs \circ -) z < 1)$
34	21 24 33	syl2anc	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to (z \in (y ball (abs \circ -) 1) \leftrightarrow y (abs \circ -) z < 1)$
35	31 34	mpbid	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y (abs \circ -) z < 1$
36	30 35	eqbrtrrd	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to \|y - z\| < 1$
37		nn0abscl	$⊢ y - z \in ℤ \to \|y - z\| \in ℕ_{0}$
38		nn0lt10b	$⊢ \|y - z\| \in ℕ_{0} \to (\|y - z\| < 1 \leftrightarrow \|y - z\| = 0)$
39	26 37 38	3syl	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to (\|y - z\| < 1 \leftrightarrow \|y - z\| = 0)$
40	36 39	mpbid	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to \|y - z\| = 0$
41	27 40	abs00d	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y - z = 0$
42	21 24 41	subeq0d	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y = z$
43		simplr	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to y \in x$
44	42 43	eqeltrrd	$⊢ ((x \in 𝒫 ℤ \land y \in x) \land z \in ((y ball (abs \circ -) 1) \cap ℤ)) \to z \in x$
45	44	ex	$⊢ (x \in 𝒫 ℤ \land y \in x) \to (z \in ((y ball (abs \circ -) 1) \cap ℤ) \to z \in x)$
46	45	ssrdv	$⊢ (x \in 𝒫 ℤ \land y \in x) \to (y ball (abs \circ -) 1) \cap ℤ \subseteq x$
47		eleq2	$⊢ z = (y ball (abs \circ -) 1) \cap ℤ \to (y \in z \leftrightarrow y \in ((y ball (abs \circ -) 1) \cap ℤ))$
48		sseq1	$⊢ z = (y ball (abs \circ -) 1) \cap ℤ \to (z \subseteq x \leftrightarrow (y ball (abs \circ -) 1) \cap ℤ \subseteq x)$
49	47 48	anbi12d	$⊢ z = (y ball (abs \circ -) 1) \cap ℤ \to ((y \in z \land z \subseteq x) \leftrightarrow (y \in ((y ball (abs \circ -) 1) \cap ℤ) \land (y ball (abs \circ -) 1) \cap ℤ \subseteq x))$
50	49	rspcev	$⊢ ((y ball (abs \circ -) 1) \cap ℤ \in (J ↾_{𝑡} ℤ) \land (y \in ((y ball (abs \circ -) 1) \cap ℤ) \land (y ball (abs \circ -) 1) \cap ℤ \subseteq x)) \to \exists z \in (J ↾_{𝑡} ℤ) (y \in z \land z \subseteq x)$
51	15 20 46 50	syl12anc	$⊢ (x \in 𝒫 ℤ \land y \in x) \to \exists z \in (J ↾_{𝑡} ℤ) (y \in z \land z \subseteq x)$
52	51	ralrimiva	$⊢ x \in 𝒫 ℤ \to \forall y \in x \exists z \in (J ↾_{𝑡} ℤ) (y \in z \land z \subseteq x)$
53		resttop	$⊢ (J \in Top \land ℤ \in V) \to J ↾_{𝑡} ℤ \in Top$
54	11 12 53	mp2an	$⊢ J ↾_{𝑡} ℤ \in Top$
55		eltop2	$⊢ J ↾_{𝑡} ℤ \in Top \to (x \in (J ↾_{𝑡} ℤ) \leftrightarrow \forall y \in x \exists z \in (J ↾_{𝑡} ℤ) (y \in z \land z \subseteq x))$
56	54 55	ax-mp	$⊢ x \in (J ↾_{𝑡} ℤ) \leftrightarrow \forall y \in x \exists z \in (J ↾_{𝑡} ℤ) (y \in z \land z \subseteq x)$
57	52 56	sylibr	$⊢ x \in 𝒫 ℤ \to x \in (J ↾_{𝑡} ℤ)$
58	57	ssriv	$⊢ 𝒫 ℤ \subseteq J ↾_{𝑡} ℤ$
59	2 58	eqssi	$⊢ J ↾_{𝑡} ℤ = 𝒫 ℤ$

Metamath Proof Explorer

Theorem zdis

Proof