Metamath Proof Explorer

Theorem iocmnfcld

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

Ref Expression
Assertion iocmnfcld ( 𝐴 ∈ ℝ → ( -∞ (,] 𝐴 ) ∈ ( 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-ioc ⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
9 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
10 xrltnle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 ↔ ¬ 𝑤 ≤ 𝐴 ) )
11 xrlelttr ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 ≤ 𝐴 ∧ 𝐴 < +∞ ) → 𝑤 < +∞ ) )
12 xrlttr ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( -∞ < 𝐴 ∧ 𝐴 < 𝑤 ) → -∞ < 𝑤 ) )
13 8 9 10 9 11 12 ixxun ⊢ ( ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 𝐴 ∧ 𝐴 < +∞ ) ) → ( ( -∞ (,] 𝐴 ) ∪ ( 𝐴 (,) +∞ ) ) = ( -∞ (,) +∞ ) )
14 2 3 5 6 7 13 syl32anc ⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,] 𝐴 ) ∪ ( 𝐴 (,) +∞ ) ) = ( -∞ (,) +∞ ) )
15 ioomax ⊢ ( -∞ (,) +∞ ) = ℝ
16 14 15 eqtrdi ⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,] 𝐴 ) ∪ ( 𝐴 (,) +∞ ) ) = ℝ )
17 iocssre ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ ) → ( -∞ (,] 𝐴 ) ⊆ ℝ )
18 1 17 mpan ⊢ ( 𝐴 ∈ ℝ → ( -∞ (,] 𝐴 ) ⊆ ℝ )
19 8 9 10 ixxdisj ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ (,] 𝐴 ) ∩ ( 𝐴 (,) +∞ ) ) = ∅ )
20 1 3 5 19 mp3an2i ⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,] 𝐴 ) ∩ ( 𝐴 (,) +∞ ) ) = ∅ )
21 uneqdifeq ⊢ ( ( ( -∞ (,] 𝐴 ) ⊆ ℝ ∧ ( ( -∞ (,] 𝐴 ) ∩ ( 𝐴 (,) +∞ ) ) = ∅ ) → ( ( ( -∞ (,] 𝐴 ) ∪ ( 𝐴 (,) +∞ ) ) = ℝ ↔ ( ℝ ∖ ( -∞ (,] 𝐴 ) ) = ( 𝐴 (,) +∞ ) ) )
22 18 20 21 syl2anc ⊢ ( 𝐴 ∈ ℝ → ( ( ( -∞ (,] 𝐴 ) ∪ ( 𝐴 (,) +∞ ) ) = ℝ ↔ ( ℝ ∖ ( -∞ (,] 𝐴 ) ) = ( 𝐴 (,) +∞ ) ) )
23 16 22 mpbid ⊢ ( 𝐴 ∈ ℝ → ( ℝ ∖ ( -∞ (,] 𝐴 ) ) = ( 𝐴 (,) +∞ ) )
24 iooretop ⊢ ( 𝐴 (,) +∞ ) ∈ ( topGen ‘ ran (,) )
25 23 24 eqeltrdi ⊢ ( 𝐴 ∈ ℝ → ( ℝ ∖ ( -∞ (,] 𝐴 ) ) ∈ ( topGen ‘ ran (,) ) )
26 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
27 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
28 27 iscld2 ⊢ ( ( ( topGen ‘ ran (,) ) ∈ Top ∧ ( -∞ (,] 𝐴 ) ⊆ ℝ ) → ( ( -∞ (,] 𝐴 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ↔ ( ℝ ∖ ( -∞ (,] 𝐴 ) ) ∈ ( topGen ‘ ran (,) ) ) )
29 26 18 28 sylancr ⊢ ( 𝐴 ∈ ℝ → ( ( -∞ (,] 𝐴 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) ↔ ( ℝ ∖ ( -∞ (,] 𝐴 ) ) ∈ ( topGen ‘ ran (,) ) ) )
30 25 29 mpbird ⊢ ( 𝐴 ∈ ℝ → ( -∞ (,] 𝐴 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )