| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . . . . 9
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) | 
| 2 |  | eqid 2737 | . . . . . . . . 9
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) | 
| 3 |  | eqid 2737 | . . . . . . . . 9
⊢ ran (,) =
ran (,) | 
| 4 | 1, 2, 3 | leordtval 23221 | . . . . . . . 8
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) | 
| 5 |  | letop 23214 | . . . . . . . 8
⊢
(ordTop‘ ≤ ) ∈ Top | 
| 6 | 4, 5 | eqeltrri 2838 | . . . . . . 7
⊢
(topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top | 
| 7 |  | tgclb 22977 | . . . . . . 7
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top) | 
| 8 | 6, 7 | mpbir 231 | . . . . . 6
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases | 
| 9 |  | bastg 22973 | . . . . . 6
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases → ((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)) ⊆ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,)))) | 
| 10 | 8, 9 | ax-mp 5 | . . . . 5
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ⊆ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) | 
| 11 | 10, 4 | sseqtrri 4033 | . . . 4
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ⊆ (ordTop‘ ≤ ) | 
| 12 |  | ssun1 4178 | . . . . 5
⊢ (ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ⊆
((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) | 
| 13 |  | ssun1 4178 | . . . . . 6
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ⊆ (ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
∪ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) | 
| 14 |  | eqid 2737 | . . . . . . . 8
⊢ (𝐴(,]+∞) = (𝐴(,]+∞) | 
| 15 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥(,]+∞) = (𝐴(,]+∞)) | 
| 16 | 15 | rspceeqv 3645 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ (𝐴(,]+∞) =
(𝐴(,]+∞)) →
∃𝑥 ∈
ℝ* (𝐴(,]+∞) = (𝑥(,]+∞)) | 
| 17 | 14, 16 | mpan2 691 | . . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ ∃𝑥 ∈
ℝ* (𝐴(,]+∞) = (𝑥(,]+∞)) | 
| 18 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) | 
| 19 |  | ovex 7464 | . . . . . . . 8
⊢ (𝑥(,]+∞) ∈
V | 
| 20 | 18, 19 | elrnmpti 5973 | . . . . . . 7
⊢ ((𝐴(,]+∞) ∈ ran (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞))
↔ ∃𝑥 ∈
ℝ* (𝐴(,]+∞) = (𝑥(,]+∞)) | 
| 21 | 17, 20 | sylibr 234 | . . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,]+∞)
∈ ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞))) | 
| 22 | 13, 21 | sselid 3981 | . . . . 5
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,]+∞)
∈ (ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)))) | 
| 23 | 12, 22 | sselid 3981 | . . . 4
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,]+∞)
∈ ((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))) | 
| 24 | 11, 23 | sselid 3981 | . . 3
⊢ (𝐴 ∈ ℝ*
→ (𝐴(,]+∞)
∈ (ordTop‘ ≤ )) | 
| 25 | 24 | adantr 480 | . 2
⊢ ((𝐴 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) ∈ (ordTop‘ ≤
)) | 
| 26 |  | df-ioc 13392 | . . . . . 6
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) | 
| 27 | 26 | ixxf 13397 | . . . . 5
⊢
(,]:(ℝ* × ℝ*)⟶𝒫
ℝ* | 
| 28 | 27 | fdmi 6747 | . . . 4
⊢ dom (,] =
(ℝ* × ℝ*) | 
| 29 | 28 | ndmov 7617 | . . 3
⊢ (¬
(𝐴 ∈
ℝ* ∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) =
∅) | 
| 30 |  | 0opn 22910 | . . . 4
⊢
((ordTop‘ ≤ ) ∈ Top → ∅ ∈ (ordTop‘
≤ )) | 
| 31 | 5, 30 | ax-mp 5 | . . 3
⊢ ∅
∈ (ordTop‘ ≤ ) | 
| 32 | 29, 31 | eqeltrdi 2849 | . 2
⊢ (¬
(𝐴 ∈
ℝ* ∧ +∞ ∈ ℝ*) → (𝐴(,]+∞) ∈
(ordTop‘ ≤ )) | 
| 33 | 25, 32 | pm2.61i 182 | 1
⊢ (𝐴(,]+∞) ∈
(ordTop‘ ≤ ) |