Metamath Proof Explorer

Theorem iooordt

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

Ref Expression
Assertion iooordt ⊢ A B ∈ 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 ssun2 ⊢ ran ⁡ . ⊆ ran ⁡ x ∈ ℝ * ⟼ x +∞ ∪ ran ⁡ x ∈ ℝ * ⟼ −∞ x ∪ ran ⁡ .
13 ioorebas ⊢ A B ∈ ran ⁡ .
14 12 13 sselii ⊢ A B ∈ ran ⁡ x ∈ ℝ * ⟼ x +∞ ∪ ran ⁡ x ∈ ℝ * ⟼ −∞ x ∪ ran ⁡ .
15 11 14 sselii ⊢ A B ∈ ordTop ⁡ ≤