zcld

Description: The integers are a closed set in the topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

		Ref	Expression
	Hypothesis	zcld.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
	Assertion	zcld	⊢ ℤ ∈ ( Clsd ‘ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		zcld.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ↔ ∃ 𝑥 ∈ ℤ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) )
3		elioore	⊢ ( 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) → 𝑦 ∈ ℝ )
4	3	adantl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) ) → 𝑦 ∈ ℝ )
5		eliooord	⊢ ( 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) → ( 𝑥 < 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) )
6		btwnnz	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑥 < 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) → ¬ 𝑦 ∈ ℤ )
7	6	3expb	⊢ ( ( 𝑥 ∈ ℤ ∧ ( 𝑥 < 𝑦 ∧ 𝑦 < ( 𝑥 + 1 ) ) ) → ¬ 𝑦 ∈ ℤ )
8	5 7	sylan2	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) ) → ¬ 𝑦 ∈ ℤ )
9	4 8	eldifd	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) ) → 𝑦 ∈ ( ℝ ∖ ℤ ) )
10	9	rexlimiva	⊢ ( ∃ 𝑥 ∈ ℤ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) → 𝑦 ∈ ( ℝ ∖ ℤ ) )
11		eldifi	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → 𝑦 ∈ ℝ )
12	11	flcld	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) ∈ ℤ )
13	12	zred	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) ∈ ℝ )
14		flle	⊢ ( 𝑦 ∈ ℝ → ( ⌊ ‘ 𝑦 ) ≤ 𝑦 )
15	11 14	syl	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) ≤ 𝑦 )
16		eldifn	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ¬ 𝑦 ∈ ℤ )
17		nelne2	⊢ ( ( ( ⌊ ‘ 𝑦 ) ∈ ℤ ∧ ¬ 𝑦 ∈ ℤ ) → ( ⌊ ‘ 𝑦 ) ≠ 𝑦 )
18	12 16 17	syl2anc	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) ≠ 𝑦 )
19	18	necomd	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → 𝑦 ≠ ( ⌊ ‘ 𝑦 ) )
20	13 11 15 19	leneltd	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) < 𝑦 )
21		flltp1	⊢ ( 𝑦 ∈ ℝ → 𝑦 < ( ( ⌊ ‘ 𝑦 ) + 1 ) )
22	11 21	syl	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → 𝑦 < ( ( ⌊ ‘ 𝑦 ) + 1 ) )
23	13	rexrd	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ⌊ ‘ 𝑦 ) ∈ ℝ^* )
24		peano2re	⊢ ( ( ⌊ ‘ 𝑦 ) ∈ ℝ → ( ( ⌊ ‘ 𝑦 ) + 1 ) ∈ ℝ )
25	13 24	syl	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ( ⌊ ‘ 𝑦 ) + 1 ) ∈ ℝ )
26	25	rexrd	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( ( ⌊ ‘ 𝑦 ) + 1 ) ∈ ℝ^* )
27		elioo2	⊢ ( ( ( ⌊ ‘ 𝑦 ) ∈ ℝ^* ∧ ( ( ⌊ ‘ 𝑦 ) + 1 ) ∈ ℝ^* ) → ( 𝑦 ∈ ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ⌊ ‘ 𝑦 ) < 𝑦 ∧ 𝑦 < ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ) )
28	23 26 27	syl2anc	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ( 𝑦 ∈ ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( ⌊ ‘ 𝑦 ) < 𝑦 ∧ 𝑦 < ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ) )
29	11 20 22 28	mpbir3and	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → 𝑦 ∈ ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) )
30		id	⊢ ( 𝑥 = ( ⌊ ‘ 𝑦 ) → 𝑥 = ( ⌊ ‘ 𝑦 ) )
31		oveq1	⊢ ( 𝑥 = ( ⌊ ‘ 𝑦 ) → ( 𝑥 + 1 ) = ( ( ⌊ ‘ 𝑦 ) + 1 ) )
32	30 31	oveq12d	⊢ ( 𝑥 = ( ⌊ ‘ 𝑦 ) → ( 𝑥 (,) ( 𝑥 + 1 ) ) = ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) )
33	32	eleq2d	⊢ ( 𝑥 = ( ⌊ ‘ 𝑦 ) → ( 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) ↔ 𝑦 ∈ ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ) )
34	33	rspcev	⊢ ( ( ( ⌊ ‘ 𝑦 ) ∈ ℤ ∧ 𝑦 ∈ ( ( ⌊ ‘ 𝑦 ) (,) ( ( ⌊ ‘ 𝑦 ) + 1 ) ) ) → ∃ 𝑥 ∈ ℤ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) )
35	12 29 34	syl2anc	⊢ ( 𝑦 ∈ ( ℝ ∖ ℤ ) → ∃ 𝑥 ∈ ℤ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) )
36	10 35	impbii	⊢ ( ∃ 𝑥 ∈ ℤ 𝑦 ∈ ( 𝑥 (,) ( 𝑥 + 1 ) ) ↔ 𝑦 ∈ ( ℝ ∖ ℤ ) )
37	2 36	bitri	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ↔ 𝑦 ∈ ( ℝ ∖ ℤ ) )
38	37	eqriv	⊢ ∪ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) = ( ℝ ∖ ℤ )
39		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
40	1 39	eqeltri	⊢ 𝐽 ∈ Top
41		iooretop	⊢ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ ( topGen ‘ ran (,) )
42	41 1	eleqtrri	⊢ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ 𝐽
43	42	rgenw	⊢ ∀ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ 𝐽
44		iunopn	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ 𝐽 ) → ∪ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ 𝐽 )
45	40 43 44	mp2an	⊢ ∪ 𝑥 ∈ ℤ ( 𝑥 (,) ( 𝑥 + 1 ) ) ∈ 𝐽
46	38 45	eqeltrri	⊢ ( ℝ ∖ ℤ ) ∈ 𝐽
47		zssre	⊢ ℤ ⊆ ℝ
48		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
49	1	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
50	48 49	eqtr4i	⊢ ℝ = ∪ 𝐽
51	50	iscld2	⊢ ( ( 𝐽 ∈ Top ∧ ℤ ⊆ ℝ ) → ( ℤ ∈ ( Clsd ‘ 𝐽 ) ↔ ( ℝ ∖ ℤ ) ∈ 𝐽 ) )
52	40 47 51	mp2an	⊢ ( ℤ ∈ ( Clsd ‘ 𝐽 ) ↔ ( ℝ ∖ ℤ ) ∈ 𝐽 )
53	46 52	mpbir	⊢ ℤ ∈ ( Clsd ‘ 𝐽 )

Metamath Proof Explorer

Theorem zcld

Proof