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 ‘ ≤ )