Step | Hyp | Ref
| Expression |
1 | | icoopn.k |
. . . . 5
⊢ 𝐾 = (topGen‘ran
(,)) |
2 | | retop 23688 |
. . . . 5
⊢
(topGen‘ran (,)) ∈ Top |
3 | 1, 2 | eqeltri 2836 |
. . . 4
⊢ 𝐾 ∈ Top |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Top) |
5 | | ovexd 7269 |
. . 3
⊢ (𝜑 → (𝐴[,)𝐵) ∈ V) |
6 | | iooretop 23692 |
. . . . 5
⊢
(-∞(,)𝐶)
∈ (topGen‘ran (,)) |
7 | 6, 1 | eleqtrri 2839 |
. . . 4
⊢
(-∞(,)𝐶)
∈ 𝐾 |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (-∞(,)𝐶) ∈ 𝐾) |
9 | | elrestr 16963 |
. . 3
⊢ ((𝐾 ∈ Top ∧ (𝐴[,)𝐵) ∈ V ∧ (-∞(,)𝐶) ∈ 𝐾) → ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) ∈ (𝐾 ↾t (𝐴[,)𝐵))) |
10 | 4, 5, 8, 9 | syl3anc 1373 |
. 2
⊢ (𝜑 → ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) ∈ (𝐾 ↾t (𝐴[,)𝐵))) |
11 | | icoopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
12 | 11 | rexrd 10910 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
13 | 12 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ∈
ℝ*) |
14 | | icoopn.c |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
15 | 14 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐶 ∈
ℝ*) |
16 | | elinel1 4125 |
. . . . . . . 8
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (-∞(,)𝐶)) |
17 | | elioore 12992 |
. . . . . . . 8
⊢ (𝑥 ∈ (-∞(,)𝐶) → 𝑥 ∈ ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ ℝ) |
19 | 18 | rexrd 10910 |
. . . . . 6
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ ℝ*) |
20 | 19 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ ℝ*) |
21 | | icoopn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
22 | 21 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐵 ∈
ℝ*) |
23 | | elinel2 4126 |
. . . . . . 7
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,)𝐵)) |
24 | 23 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐵)) |
25 | | icogelb 13013 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝑥) |
26 | 13, 22, 24, 25 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ≤ 𝑥) |
27 | | mnfxr 10917 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → -∞ ∈
ℝ*) |
29 | 16 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (-∞(,)𝐶)) |
30 | | iooltub 42756 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝐶)) → 𝑥 < 𝐶) |
31 | 28, 15, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 < 𝐶) |
32 | 13, 15, 20, 26, 31 | elicod 13012 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐶)) |
33 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ ∈
ℝ*) |
34 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ∈
ℝ*) |
35 | | icossre 13043 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ*)
→ (𝐴[,)𝐶) ⊆
ℝ) |
36 | 11, 14, 35 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,)𝐶) ⊆ ℝ) |
37 | 36 | sselda 3917 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ) |
38 | 37 | mnfltd 12743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ < 𝑥) |
39 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ∈
ℝ*) |
40 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐶)) |
41 | | icoltub 42754 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
42 | 39, 34, 40, 41 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
43 | 33, 34, 37, 38, 42 | eliood 42744 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (-∞(,)𝐶)) |
44 | 21 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐵 ∈
ℝ*) |
45 | 37 | rexrd 10910 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ*) |
46 | | icogelb 13013 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
47 | 39, 34, 40, 46 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
48 | | icoopn.cleb |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ 𝐵) |
49 | 48 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ≤ 𝐵) |
50 | 45, 34, 44, 42, 49 | xrltletrd 12778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐵) |
51 | 39, 44, 45, 47, 50 | elicod 13012 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐵)) |
52 | 43, 51 | elind 4124 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) |
53 | 32, 52 | impbida 801 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) ↔ 𝑥 ∈ (𝐴[,)𝐶))) |
54 | 53 | eqrdv 2737 |
. 2
⊢ (𝜑 → ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) = (𝐴[,)𝐶)) |
55 | | icoopn.j |
. . . 4
⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵)) |
56 | 55 | eqcomi 2748 |
. . 3
⊢ (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽 |
57 | 56 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽) |
58 | 10, 54, 57 | 3eltr3d 2854 |
1
⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽) |