Step | Hyp | Ref
| Expression |
1 | | iocopn.k |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
2 | | retop 22375 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
3 | 1, 2 | eqeltri 2684 |
. . . 4
⊢ 𝐾 ∈ Top |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | ovex 6577 |
. . . 4
⊢ (𝐴(,]𝐵) ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐴(,]𝐵) ∈ V) |
7 | | iooretop 22379 |
. . . . 5
⊢ (𝐶(,)+∞) ∈
(topGen‘ran (,)) |
8 | 7, 1 | eleqtrri 2687 |
. . . 4
⊢ (𝐶(,)+∞) ∈ 𝐾 |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → (𝐶(,)+∞) ∈ 𝐾) |
10 | | elrestr 15912 |
. . 3
⊢ ((𝐾 ∈ Top ∧ (𝐴(,]𝐵) ∈ V ∧ (𝐶(,)+∞) ∈ 𝐾) → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ∈ (𝐾 ↾t (𝐴(,]𝐵))) |
11 | 4, 6, 9, 10 | syl3anc 1318 |
. 2
⊢ (𝜑 → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ∈ (𝐾 ↾t (𝐴(,]𝐵))) |
12 | | iocopn.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 ∈
ℝ*) |
14 | | iocopn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
15 | 14 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐵 ∈
ℝ*) |
17 | | elinel1 3761 |
. . . . . . . 8
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) |
18 | | elioore 12076 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐶(,)+∞) → 𝑥 ∈ ℝ) |
19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ) |
20 | 19 | rexrd 9968 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ ℝ*) |
21 | 20 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ ℝ*) |
22 | | pnfxr 9971 |
. . . . . . 7
⊢ +∞
∈ ℝ* |
23 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → +∞ ∈
ℝ*) |
24 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,)+∞)) |
25 | | ioogtlb 38564 |
. . . . . 6
⊢ ((𝐶 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑥 ∈ (𝐶(,)+∞)) → 𝐶 < 𝑥) |
26 | 13, 23, 24, 25 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐶 < 𝑥) |
27 | | iocopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
28 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝐴 ∈
ℝ*) |
29 | | elinel2 3762 |
. . . . . . 7
⊢ (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) |
30 | 29 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐴(,]𝐵)) |
31 | | iocleub 38572 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴(,]𝐵)) → 𝑥 ≤ 𝐵) |
32 | 28, 16, 30, 31 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ≤ 𝐵) |
33 | 13, 16, 21, 26, 32 | eliocd 38577 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) → 𝑥 ∈ (𝐶(,]𝐵)) |
34 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 ∈
ℝ*) |
35 | 22 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → +∞ ∈
ℝ*) |
36 | | iocopn.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | | iocssre 12124 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐶(,]𝐵) ⊆
ℝ) |
38 | 12, 36, 37 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐶(,]𝐵) ⊆ ℝ) |
39 | 38 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ℝ) |
40 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐵 ∈
ℝ*) |
41 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,]𝐵)) |
42 | | iocgtlb 38571 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐶(,]𝐵)) → 𝐶 < 𝑥) |
43 | 34, 40, 41, 42 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐶 < 𝑥) |
44 | 39 | ltpnfd 11831 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 < +∞) |
45 | 34, 35, 39, 43, 44 | eliood 38567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐶(,)+∞)) |
46 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ∈
ℝ*) |
47 | 39 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ℝ*) |
48 | | iocopn.alec |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ 𝐶) |
49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 ≤ 𝐶) |
50 | 46, 34, 47, 49, 43 | xrlelttrd 11867 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝐴 < 𝑥) |
51 | | iocleub 38572 |
. . . . . . 7
⊢ ((𝐶 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐶(,]𝐵)) → 𝑥 ≤ 𝐵) |
52 | 34, 40, 41, 51 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ≤ 𝐵) |
53 | 46, 40, 47, 50, 52 | eliocd 38577 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ (𝐴(,]𝐵)) |
54 | 45, 53 | elind 3760 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐶(,]𝐵)) → 𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵))) |
55 | 33, 54 | impbida 873 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) ↔ 𝑥 ∈ (𝐶(,]𝐵))) |
56 | 55 | eqrdv 2608 |
. 2
⊢ (𝜑 → ((𝐶(,)+∞) ∩ (𝐴(,]𝐵)) = (𝐶(,]𝐵)) |
57 | | iocopn.j |
. . . 4
⊢ 𝐽 = (𝐾 ↾t (𝐴(,]𝐵)) |
58 | 57 | eqcomi 2619 |
. . 3
⊢ (𝐾 ↾t (𝐴(,]𝐵)) = 𝐽 |
59 | 58 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ↾t (𝐴(,]𝐵)) = 𝐽) |
60 | 11, 56, 59 | 3eltr3d 2702 |
1
⊢ (𝜑 → (𝐶(,]𝐵) ∈ 𝐽) |