This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 (,) 𝐵 ) ∈ ( ordTop ‘ ≤ )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
2 eqid ⊢ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
3 eqid ⊢ ran (,) = ran (,)
4 1 2 3 leordtval ⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) )
5 letop ⊢ ( ordTop ‘ ≤ ) ∈ Top
6 4 5 eqeltrri ⊢ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ∈ Top
7 tgclb ⊢ ( ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases ↔ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ∈ Top )
8 6 7 mpbir ⊢ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases
9 bastg ⊢ ( ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases → ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ⊆ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) )
10 8 9 ax-mp ⊢ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ⊆ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) )
11 10 4 sseqtrri ⊢ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ⊆ ( ordTop ‘ ≤ )
12 ssun2 ⊢ ran (,) ⊆ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) )
13 ioorebas ⊢ ( 𝐴 (,) 𝐵 ) ∈ ran (,)
14 12 13 sselii ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) )
15 11 14 sselii ⊢ ( 𝐴 (,) 𝐵 ) ∈ ( ordTop ‘ ≤ )