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⁡.