Metamath Proof Explorer

Theorem icomnfordt

Description: An unbounded above open interval is open in the order topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion icomnfordt ⊢−∞A∈ordTop⁡≤

Proof

Step Hyp Ref Expression
1 eqid ⊢ran⁡x∈ℝ*⟼x+∞=ran⁡x∈ℝ*⟼x+∞
2 eqid ⊢ran⁡x∈ℝ*⟼−∞x=ran⁡x∈ℝ*⟼−∞x
3 eqid ⊢ran⁡.=ran⁡.
4 1 2 3 leordtval ⊢ordTop⁡≤=topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
5 letop ⊢ordTop⁡≤∈Top
6 4 5 eqeltrri ⊢topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈Top
7 tgclb ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases↔topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈Top
8 6 7 mpbir ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases
9 bastg ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.∈TopBases→ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.⊆topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
10 8 9 ax-mp ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.⊆topGen⁡ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
11 10 4 sseqtrri ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.⊆ordTop⁡≤
12 ssun1 ⊢ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x⊆ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
13 ssun2 ⊢ran⁡x∈ℝ*⟼−∞x⊆ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x
14 eqid ⊢−∞A=−∞A
15 oveq2 ⊢x=A→−∞x=−∞A
16 15 rspceeqv ⊢A∈ℝ*∧−∞A=−∞A→∃x∈ℝ*−∞A=−∞x
17 14 16 mpan2 ⊢A∈ℝ*→∃x∈ℝ*−∞A=−∞x
18 eqid ⊢x∈ℝ*⟼−∞x=x∈ℝ*⟼−∞x
19 ovex ⊢−∞x∈V
20 18 19 elrnmpti ⊢−∞A∈ran⁡x∈ℝ*⟼−∞x↔∃x∈ℝ*−∞A=−∞x
21 17 20 sylibr ⊢A∈ℝ*→−∞A∈ran⁡x∈ℝ*⟼−∞x
22 13 21 sselid ⊢A∈ℝ*→−∞A∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x
23 12 22 sselid ⊢A∈ℝ*→−∞A∈ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x∪ran⁡.
24 11 23 sselid ⊢A∈ℝ*→−∞A∈ordTop⁡≤
25 24 adantl ⊢−∞∈ℝ*∧A∈ℝ*→−∞A∈ordTop⁡≤
26 df-ico ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x≤z∧z<y
27 26 ixxf ⊢.:ℝ*×ℝ*⟶𝒫ℝ*
28 27 fdmi ⊢dom⁡.=ℝ*×ℝ*
29 28 ndmov ⊢¬−∞∈ℝ*∧A∈ℝ*→−∞A=∅
30 0opn ⊢ordTop⁡≤∈Top→∅∈ordTop⁡≤
31 5 30 ax-mp ⊢∅∈ordTop⁡≤
32 29 31 eqeltrdi ⊢¬−∞∈ℝ*∧A∈ℝ*→−∞A∈ordTop⁡≤
33 25 32 pm2.61i ⊢−∞A∈ordTop⁡≤