| Step | Hyp | Ref
| Expression |
| 1 | | icoopn.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 | | icoopn.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 12 | 11 | rexrd 11311 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ∈
ℝ*) |
| 14 | | icoopn.c |
. . . . . 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 | | icoopn.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐵 ∈
ℝ*) |
| 23 | | elinel2 4202 |
. . . . . . 7
⊢ (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) → 𝑥 ∈ (𝐴[,)𝐵)) |
| 24 | 23 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐵)) |
| 25 | | icogelb 13438 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐵)) → 𝐴 ≤ 𝑥) |
| 26 | 13, 22, 24, 25 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝐴 ≤ 𝑥) |
| 27 | | mnfxr 11318 |
. . . . . . 7
⊢ -∞
∈ ℝ* |
| 28 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → -∞ ∈
ℝ*) |
| 29 | 16 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (-∞(,)𝐶)) |
| 30 | | iooltub 45523 |
. . . . . 6
⊢
((-∞ ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑥 ∈ (-∞(,)𝐶)) → 𝑥 < 𝐶) |
| 31 | 28, 15, 29, 30 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 < 𝐶) |
| 32 | 13, 15, 20, 26, 31 | elicod 13437 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) → 𝑥 ∈ (𝐴[,)𝐶)) |
| 33 | 27 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ ∈
ℝ*) |
| 34 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ∈
ℝ*) |
| 35 | | icossre 13468 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ*)
→ (𝐴[,)𝐶) ⊆
ℝ) |
| 36 | 11, 14, 35 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,)𝐶) ⊆ ℝ) |
| 37 | 36 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ) |
| 38 | 37 | mnfltd 13166 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → -∞ < 𝑥) |
| 39 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ∈
ℝ*) |
| 40 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐶)) |
| 41 | | icoltub 45521 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
| 42 | 39, 34, 40, 41 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐶) |
| 43 | 33, 34, 37, 38, 42 | eliood 45511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (-∞(,)𝐶)) |
| 44 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐵 ∈
ℝ*) |
| 45 | 37 | rexrd 11311 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ℝ*) |
| 46 | | icogelb 13438 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
| 47 | 39, 34, 40, 46 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐴 ≤ 𝑥) |
| 48 | | icoopn.cleb |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ 𝐵) |
| 49 | 48 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝐶 ≤ 𝐵) |
| 50 | 45, 34, 44, 42, 49 | xrltletrd 13203 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 < 𝐵) |
| 51 | 39, 44, 45, 47, 50 | elicod 13437 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ (𝐴[,)𝐵)) |
| 52 | 43, 51 | elind 4200 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,)𝐶)) → 𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵))) |
| 53 | 32, 52 | impbida 801 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) ↔ 𝑥 ∈ (𝐴[,)𝐶))) |
| 54 | 53 | eqrdv 2735 |
. 2
⊢ (𝜑 → ((-∞(,)𝐶) ∩ (𝐴[,)𝐵)) = (𝐴[,)𝐶)) |
| 55 | | icoopn.j |
. . . 4
⊢ 𝐽 = (𝐾 ↾t (𝐴[,)𝐵)) |
| 56 | 55 | eqcomi 2746 |
. . 3
⊢ (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽 |
| 57 | 56 | a1i 11 |
. 2
⊢ (𝜑 → (𝐾 ↾t (𝐴[,)𝐵)) = 𝐽) |
| 58 | 10, 54, 57 | 3eltr3d 2855 |
1
⊢ (𝜑 → (𝐴[,)𝐶) ∈ 𝐽) |