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