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

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 ( 𝐴 (,] +∞ ) ∈ ( 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 ssun1 ⊢ ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ⊆ ( ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) )
14 eqid ⊢ ( 𝐴 (,] +∞ ) = ( 𝐴 (,] +∞ )
15 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 (,] +∞ ) = ( 𝐴 (,] +∞ ) )
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 adantr ⊢ ( ( 𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝐴 (,] +∞ ) ∈ ( ordTop ‘ ≤ ) )
26 df-ioc ⊢ (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
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 ‘ ≤ )