Theorem icopnfcld

Description: Right-unbounded closed intervals are closed sets of the standard topology on RR . (Contributed by Mario Carneiro, 17-Feb-2015)

	Ref	Expression
Assertion	icopnfcld	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2	1	a1i	⊢ ( 𝐴 ∈ ℝ → -∞ ∈ ℝ* )
3		rexr	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
4		pnfxr	⊢ +∞ ∈ ℝ*
5	4	a1i	⊢ ( 𝐴 ∈ ℝ → +∞ ∈ ℝ* )
6		mnflt	⊢ ( 𝐴 ∈ ℝ → -∞ < 𝐴 )
7		ltpnf	⊢ ( 𝐴 ∈ ℝ → 𝐴 < +∞ )
8		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
9		df-ico	⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
10		xrlenlt	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 ≤ 𝑤 ↔ ¬ 𝑤 < 𝐴 ) )
11		xrlttr	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 < 𝐴 ∧ 𝐴 < +∞ ) → 𝑤 < +∞ ) )
12		xrltletr	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( -∞ < 𝐴 ∧ 𝐴 ≤ 𝑤 ) → -∞ < 𝑤 ) )
13	8 9 10 8 11 12	ixxun	⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 𝐴 ∧ 𝐴 < +∞ ) ) → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐴 [,) +∞ ) ) = ( -∞ (,) +∞ ) )
14	2 3 5 6 7 13	syl32anc	⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐴 [,) +∞ ) ) = ( -∞ (,) +∞ ) )
15		ioomax	⊢ ( -∞ (,) +∞ ) = ℝ
16	14 15	eqtrdi	⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,) 𝐴 ) ∪ ( 𝐴 [,) +∞ ) ) = ℝ )
17		ioossre	⊢ ( -∞ (,) 𝐴 ) ⊆ ℝ
18	8 9 10	ixxdisj	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ (,) 𝐴 ) ∩ ( 𝐴 [,) +∞ ) ) = ∅ )
19	1 3 5 18	mp3an2i	⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,) 𝐴 ) ∩ ( 𝐴 [,) +∞ ) ) = ∅ )
20		uneqdifeq	⊢ ( ( ( -∞ (,) 𝐴 ) ⊆ ℝ ∧ ( ( -∞ (,) 𝐴 ) ∩ ( 𝐴 [,) +∞ ) ) = ∅ ) → ( ( ( -∞ (,) 𝐴 ) ∪ ( 𝐴 [,) +∞ ) ) = ℝ ↔ ( ℝ ∖ ( -∞ (,) 𝐴 ) ) = ( 𝐴 [,) +∞ ) ) )
21	17 19 20	sylancr	⊢ ( 𝐴 ∈ ℝ → ( ( ( -∞ (,) 𝐴 ) ∪ ( 𝐴 [,) +∞ ) ) = ℝ ↔ ( ℝ ∖ ( -∞ (,) 𝐴 ) ) = ( 𝐴 [,) +∞ ) ) )
22	16 21	mpbid	⊢ ( 𝐴 ∈ ℝ → ( ℝ ∖ ( -∞ (,) 𝐴 ) ) = ( 𝐴 [,) +∞ ) )
23		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
24		iooretop	⊢ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) )
25		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
26	25	opncld	⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,) 𝐴 ) ∈ ( topGen ‘ ran (,) ) ) → ( ℝ ∖ ( -∞ (,) 𝐴 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
27	23 24 26	mp2an	⊢ ( ℝ ∖ ( -∞ (,) 𝐴 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) )
28	22 27	eqeltrrdi	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 [,) +∞ ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )