| Step | Hyp | Ref
| Expression |
| 1 | | iocopn.k |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
| 2 | | retop 24782 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
| 3 | 1, 2 | eqeltri 2837 |
. . . 4
⊢ 𝐾 ∈ Top |
| 4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Top) |
| 5 | | ovexd 7466 |
. . 3
⊢ (𝜑 → (𝐴(,]𝐵) ∈ V) |
| 6 | | iooretop 24786 |
. . . . 5
⊢ (𝐶(,)+∞) ∈
(topGen‘ran (,)) |
| 7 | 6, 1 | eleqtrri 2840 |
. . . 4
⊢ (𝐶(,)+∞) ∈ 𝐾 |
| 8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐶(,)+∞) ∈ 𝐾) |
| 9 | | elrestr 17473 |
. . 3
⊢ ((𝐾 ∈ Top ∧ (𝐴(,]𝐵) ∈ V ∧ (𝐶(,)+∞) ∈ 𝐾) → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ∈ (𝐾 ↾t (𝐴(,]𝐵))) |
| 10 | 4, 5, 8, 9 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ∈ (𝐾 ↾t (𝐴(,]𝐵))) |
| 11 | | iocopn.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 12 | 11 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 ∈
ℝ*) |
| 13 | | iocopn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 14 | 13 | rexrd 11311 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 15 | 14 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐵 ∈
ℝ*) |
| 16 | | elinel1 4201 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) |
| 17 | | elioore 13417 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐶(,)+∞) → 𝑥 ∈ ℝ) |
| 18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ) |
| 19 | 18 | rexrd 11311 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ*) |
| 20 | 19 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ ℝ*) |
| 21 | | pnfxr 11315 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
| 22 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → +∞ ∈
ℝ*) |
| 23 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,)+∞)) |
| 24 | | ioogtlb 45508 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐶(,)+∞)) → 𝐶 < 𝑥) |
| 25 | 12, 22, 23, 24 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 < 𝑥) |
| 26 | | iocopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐴 ∈
ℝ*) |
| 28 | | elinel2 4202 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) |
| 29 | 28 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐴(,]𝐵)) |
| 30 | | iocleub 45516 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴(,]𝐵)) → 𝑥 ≤ 𝐵) |
| 31 | 27, 15, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ≤ 𝐵) |
| 32 | 12, 15, 20, 25, 31 | eliocd 45520 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,]𝐵)) |
| 33 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 ∈
ℝ*) |
| 34 | 21 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → +∞ ∈
ℝ*) |
| 35 | | iocopn.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 36 | | iocssre 13467 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐶(,]𝐵) ⊆
ℝ) |
| 37 | 11, 35, 36 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐶(,]𝐵) ⊆ ℝ) |
| 38 | 37 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ℝ) |
| 39 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐵 ∈
ℝ*) |
| 40 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,]𝐵)) |
| 41 | | iocgtlb 45515 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐶(,]𝐵)) → 𝐶 < 𝑥) |
| 42 | 33, 39, 40, 41 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 < 𝑥) |
| 43 | 38 | ltpnfd 13163 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 < +∞) |
| 44 | 33, 34, 38, 42, 43 | eliood 45511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) |
| 45 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ∈
ℝ*) |
| 46 | 38 | rexrd 11311 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ℝ*) |
| 47 | | iocopn.alec |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ 𝐶) |
| 48 | 47 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ≤ 𝐶) |
| 49 | 45, 33, 46, 48, 42 | xrlelttrd 13202 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 < 𝑥) |
| 50 | | iocleub 45516 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐶(,]𝐵)) → 𝑥 ≤ 𝐵) |
| 51 | 33, 39, 40, 50 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ≤ 𝐵) |
| 52 | 45, 39, 46, 49, 51 | eliocd 45520 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) |
| 53 | 44, 52 | elind 4200 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) |
| 54 | 32, 53 | impbida 801 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ↔ 𝑥 ∈ (𝐶(,]𝐵))) |
| 55 | 54 | eqrdv 2735 |
. 2
⊢ (𝜑 → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) = (𝐶(,]𝐵)) |
| 56 | | iocopn.j |
. . . 4
⊢ 𝐽 = (𝐾 ↾t (𝐴(,]𝐵)) |
| 57 | 56 | eqcomi 2746 |
. . 3
⊢ (𝐾 ↾t (𝐴(,]𝐵)) = 𝐽 |
| 58 | 57 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ↾t (𝐴(,]𝐵)) = 𝐽) |
| 59 | 10, 55, 58 | 3eltr3d 2855 |
1
⊢ (𝜑 → (𝐶(,]𝐵) ∈ 𝐽) |