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

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 ( -∞ [,) 𝐴 ) ∈ ( 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 ssun1 ⊢ ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ⊆ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) )
13 ssun2 ⊢ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ⊆ ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) )
14 eqid ⊢ ( -∞ [,) 𝐴 ) = ( -∞ [,) 𝐴 )
15 oveq2 ⊢ ( 𝑥 = 𝐴 → ( -∞ [,) 𝑥 ) = ( -∞ [,) 𝐴 ) )
16 15 rspceeqv ⊢ ( ( 𝐴 ∈ ℝ* ∧ ( -∞ [,) 𝐴 ) = ( -∞ [,) 𝐴 ) ) → ∃ 𝑥 ∈ ℝ* ( -∞ [,) 𝐴 ) = ( -∞ [,) 𝑥 ) )
17 14 16 mpan2 ⊢ ( 𝐴 ∈ ℝ* → ∃ 𝑥 ∈ ℝ* ( -∞ [,) 𝐴 ) = ( -∞ [,) 𝑥 ) )
18 eqid ⊢ ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) = ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
19 ovex ⊢ ( -∞ [,) 𝑥 ) ∈ V
20 18 19 elrnmpti ⊢ ( ( -∞ [,) 𝐴 ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( -∞ [,) 𝐴 ) = ( -∞ [,) 𝑥 ) )
21 17 20 sylibr ⊢ ( 𝐴 ∈ ℝ* → ( -∞ [,) 𝐴 ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) )
22 13 21 sselid ⊢ ( 𝐴 ∈ ℝ* → ( -∞ [,) 𝐴 ) ∈ ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) )
23 12 22 sselid ⊢ ( 𝐴 ∈ ℝ* → ( -∞ [,) 𝐴 ) ∈ ( ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) )
24 11 23 sselid ⊢ ( 𝐴 ∈ ℝ* → ( -∞ [,) 𝐴 ) ∈ ( ordTop ‘ ≤ ) )
25 24 adantl ⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ [,) 𝐴 ) ∈ ( ordTop ‘ ≤ ) )
26 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
27 26 ixxf ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
28 27 fdmi ⊢ dom [,) = ( ℝ* × ℝ* )
29 28 ndmov ⊢ ( ¬ ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ [,) 𝐴 ) = ∅ )
30 0opn ⊢ ( ( ordTop ‘ ≤ ) ∈ Top → ∅ ∈ ( ordTop ‘ ≤ ) )
31 5 30 ax-mp ⊢ ∅ ∈ ( ordTop ‘ ≤ )
32 29 31 eqeltrdi ⊢ ( ¬ ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ [,) 𝐴 ) ∈ ( ordTop ‘ ≤ ) )
33 25 32 pm2.61i ⊢ ( -∞ [,) 𝐴 ) ∈ ( ordTop ‘ ≤ )