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

Metamath Proof Explorer

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 (,) ) ) )