Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . . . 9
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
2 | | eqid 2610 |
. . . . . . . . 9
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
3 | | eqid 2610 |
. . . . . . . . 9
⊢ ran (,) =
ran (,) |
4 | 1, 2, 3 | leordtval 20827 |
. . . . . . . 8
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) |
5 | | letop 20820 |
. . . . . . . 8
⊢
(ordTop‘ ≤ ) ∈ Top |
6 | 4, 5 | eqeltrri 2685 |
. . . . . . 7
⊢
(topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top |
7 | | tgclb 20585 |
. . . . . . 7
⊢ (((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases ↔ (topGen‘((ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)))
∪ ran (,))) ∈ Top) |
8 | 6, 7 | mpbir 220 |
. . . . . 6
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ∈ TopBases |
9 | | bastg 20581 |
. . . . . 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 | sseqtr4i 3601 |
. . . 4
⊢ ((ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) ⊆ (ordTop‘ ≤ ) |
12 | | ssun1 3738 |
. . . . 5
⊢ (ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ⊆
((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,)) |
13 | | ssun2 3739 |
. . . . . 6
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) ⊆ (ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥))) |
14 | | eqid 2610 |
. . . . . . . 8
⊢
(-∞[,)𝐴) =
(-∞[,)𝐴) |
15 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (-∞[,)𝑥) = (-∞[,)𝐴)) |
16 | 15 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((-∞[,)𝐴) = (-∞[,)𝑥) ↔ (-∞[,)𝐴) = (-∞[,)𝐴))) |
17 | 16 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ (-∞[,)𝐴) =
(-∞[,)𝐴)) →
∃𝑥 ∈
ℝ* (-∞[,)𝐴) = (-∞[,)𝑥)) |
18 | 14, 17 | mpan2 703 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ ∃𝑥 ∈
ℝ* (-∞[,)𝐴) = (-∞[,)𝑥)) |
19 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) |
20 | | ovex 6577 |
. . . . . . . 8
⊢
(-∞[,)𝑥)
∈ V |
21 | 19, 20 | elrnmpti 5297 |
. . . . . . 7
⊢
((-∞[,)𝐴)
∈ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) ↔ ∃𝑥 ∈ ℝ* (-∞[,)𝐴) = (-∞[,)𝑥)) |
22 | 18, 21 | sylibr 223 |
. . . . . 6
⊢ (𝐴 ∈ ℝ*
→ (-∞[,)𝐴)
∈ ran (𝑥 ∈
ℝ* ↦ (-∞[,)𝑥))) |
23 | 13, 22 | sseldi 3566 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (-∞[,)𝐴)
∈ (ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)))) |
24 | 12, 23 | sseldi 3566 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (-∞[,)𝐴)
∈ ((ran (𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ∪ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥))) ∪ ran
(,))) |
25 | 11, 24 | sseldi 3566 |
. . 3
⊢ (𝐴 ∈ ℝ*
→ (-∞[,)𝐴)
∈ (ordTop‘ ≤ )) |
26 | 25 | adantl 481 |
. 2
⊢
((-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) →
(-∞[,)𝐴) ∈
(ordTop‘ ≤ )) |
27 | | df-ico 12052 |
. . . . . 6
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
28 | 27 | ixxf 12056 |
. . . . 5
⊢
[,):(ℝ* × ℝ*)⟶𝒫
ℝ* |
29 | 28 | fdmi 5965 |
. . . 4
⊢ dom [,) =
(ℝ* × ℝ*) |
30 | 29 | ndmov 6716 |
. . 3
⊢ (¬
(-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) →
(-∞[,)𝐴) =
∅) |
31 | | 0opn 20534 |
. . . 4
⊢
((ordTop‘ ≤ ) ∈ Top → ∅ ∈ (ordTop‘
≤ )) |
32 | 5, 31 | ax-mp 5 |
. . 3
⊢ ∅
∈ (ordTop‘ ≤ ) |
33 | 30, 32 | syl6eqel 2696 |
. 2
⊢ (¬
(-∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ*) →
(-∞[,)𝐴) ∈
(ordTop‘ ≤ )) |
34 | 26, 33 | pm2.61i 175 |
1
⊢
(-∞[,)𝐴)
∈ (ordTop‘ ≤ ) |