Metamath Proof Explorer

Theorem iocpnfordt

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 iocpnfordt ⊢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 ssun1 ⊢ran⁡x∈ℝ*⟼x+∞⊆ran⁡x∈ℝ*⟼x+∞∪ran⁡x∈ℝ*⟼−∞x
14 eqid ⊢A+∞=A+∞
15 oveq1 ⊢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 adantr ⊢A∈ℝ*∧+∞∈ℝ*→A+∞∈ordTop⁡≤
26 df-ioc ⊢.=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⁡≤