Step | Hyp | Ref
| Expression |
1 | | icoopn.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 | | icoopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
13 | 12 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ∈
ℝ*) |
15 | | icoopn.c |
. . . . . 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 | | icoopn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐵 ∈
ℝ*) |
24 | | elinel2 3762 |
. . . . . . 7
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,)𝐵)) |
25 | 24 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐵)) |
26 | | icogelb 12096 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝑥) |
27 | 14, 23, 25, 26 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ≤ 𝑥) |
28 | | mnfxr 9975 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
29 | 28 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → -∞ ∈
ℝ*) |
30 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (-∞(,)𝐶)) |
31 | | iooltub 38582 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝐶)) → 𝑥 < 𝐶) |
32 | 29, 16, 30, 31 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 < 𝐶) |
33 | 14, 16, 21, 27, 32 | elicod 12095 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐶)) |
34 | 28 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ ∈
ℝ*) |
35 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ∈
ℝ*) |
36 | | icossre 12125 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ*)
→ (𝐴[,)𝐶) ⊆
ℝ) |
37 | 12, 15, 36 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,)𝐶) ⊆ ℝ) |
38 | 37 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ) |
39 | 38 | mnfltd 11834 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ < 𝑥) |
40 | 13 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ∈
ℝ*) |
41 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐶)) |
42 | | icoltub 38579 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
43 | 40, 35, 41, 42 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
44 | 34, 35, 38, 39, 43 | eliood 38567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (-∞(,)𝐶)) |
45 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐵 ∈
ℝ*) |
46 | 38 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ*) |
47 | | icogelb 12096 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
48 | 40, 35, 41, 47 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
49 | | icoopn.cleb |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ 𝐵) |
50 | 49 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ≤ 𝐵) |
51 | 46, 35, 45, 43, 50 | xrltletrd 11868 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐵) |
52 | 40, 45, 46, 48, 51 | elicod 12095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐵)) |
53 | 44, 52 | elind 3760 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) |
54 | 33, 53 | impbida 873 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) ↔ 𝑥 ∈ (𝐴[,)𝐶))) |
55 | 54 | eqrdv 2608 |
. 2
⊢ (𝜑 → ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) = (𝐴[,)𝐶)) |
56 | | icoopn.j |
. . . 4
⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵)) |
57 | 56 | eqcomi 2619 |
. . 3
⊢ (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽 |
58 | 57 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽) |
59 | 11, 55, 58 | 3eltr3d 2702 |
1
⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽) |