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 ⊢ A ∈ ℝ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .

Proof

Step Hyp Ref Expression
1 mnfxr ⊢ −∞ ∈ ℝ *
2 1 a1i ⊢ A ∈ ℝ → −∞ ∈ ℝ *
3 rexr ⊢ A ∈ ℝ → A ∈ ℝ *
4 pnfxr ⊢ +∞ ∈ ℝ *
5 4 a1i ⊢ A ∈ ℝ → +∞ ∈ ℝ *
6 mnflt ⊢ A ∈ ℝ → −∞ < A
7 ltpnf ⊢ A ∈ ℝ → A < +∞
8 df-ioc ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z ≤ y
9 df-ioo ⊢ . = x ∈ ℝ * , y ∈ ℝ * ⟼ z ∈ ℝ * | x < z ∧ z < y
10 xrltnle ⊢ A ∈ ℝ * ∧ w ∈ ℝ * → A < w ↔ ¬ w ≤ A
11 xrlelttr ⊢ w ∈ ℝ * ∧ A ∈ ℝ * ∧ +∞ ∈ ℝ * → w ≤ A ∧ A < +∞ → w < +∞
12 xrlttr ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ * ∧ w ∈ ℝ * → −∞ < A ∧ A < w → −∞ < w
13 8 9 10 9 11 12 ixxun ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ −∞ < A ∧ A < +∞ → −∞ A ∪ A +∞ = −∞ +∞
14 2 3 5 6 7 13 syl32anc ⊢ A ∈ ℝ → −∞ A ∪ A +∞ = −∞ +∞
15 ioomax ⊢ −∞ +∞ = ℝ
16 14 15 eqtrdi ⊢ A ∈ ℝ → −∞ A ∪ A +∞ = ℝ
17 iocssre ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ → −∞ A ⊆ ℝ
18 1 17 mpan ⊢ A ∈ ℝ → −∞ A ⊆ ℝ
19 8 9 10 ixxdisj ⊢ −∞ ∈ ℝ * ∧ A ∈ ℝ * ∧ +∞ ∈ ℝ * → −∞ A ∩ A +∞ = ∅
20 1 3 5 19 mp3an2i ⊢ A ∈ ℝ → −∞ A ∩ A +∞ = ∅
21 uneqdifeq ⊢ −∞ A ⊆ ℝ ∧ −∞ A ∩ A +∞ = ∅ → −∞ A ∪ A +∞ = ℝ ↔ ℝ ∖ −∞ A = A +∞
22 18 20 21 syl2anc ⊢ A ∈ ℝ → −∞ A ∪ A +∞ = ℝ ↔ ℝ ∖ −∞ A = A +∞
23 16 22 mpbid ⊢ A ∈ ℝ → ℝ ∖ −∞ A = A +∞
24 iooretop ⊢ A +∞ ∈ topGen ⁡ ran ⁡ .
25 23 24 eqeltrdi ⊢ A ∈ ℝ → ℝ ∖ −∞ A ∈ topGen ⁡ ran ⁡ .
26 retop ⊢ topGen ⁡ ran ⁡ . ∈ Top
27 uniretop ⊢ ℝ = ⋃ topGen ⁡ ran ⁡ .
28 27 iscld2 ⊢ topGen ⁡ ran ⁡ . ∈ Top ∧ −∞ A ⊆ ℝ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ↔ ℝ ∖ −∞ A ∈ topGen ⁡ ran ⁡ .
29 26 18 28 sylancr ⊢ A ∈ ℝ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ . ↔ ℝ ∖ −∞ A ∈ topGen ⁡ ran ⁡ .
30 25 29 mpbird ⊢ A ∈ ℝ → −∞ A ∈ Clsd ⁡ topGen ⁡ ran ⁡ .