| Step | Hyp | Ref
| Expression |
| 1 | | icccmp.2 |
. 2
⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) |
| 2 | | icccmp.1 |
. . . . . . . 8
⊢ 𝐽 = (topGen‘ran
(,)) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
| 5 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → 𝐴 ∈ ℝ) |
| 6 | | simpllr 776 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → 𝐵 ∈ ℝ) |
| 7 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → 𝐴 ≤ 𝐵) |
| 8 | | elpwi 4607 |
. . . . . . . . 9
⊢ (𝑢 ∈ 𝒫 𝐽 → 𝑢 ⊆ 𝐽) |
| 9 | 8 | ad2antrl 728 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → 𝑢 ⊆ 𝐽) |
| 10 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → (𝐴[,]𝐵) ⊆ ∪ 𝑢) |
| 11 | 2, 1, 3, 4, 5, 6, 7, 9, 10 | icccmplem3 24846 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → 𝐵 ∈ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧}) |
| 12 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐵 → (𝐴[,]𝑥) = (𝐴[,]𝐵)) |
| 13 | 12 | sseq1d 4015 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → ((𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ (𝐴[,]𝐵) ⊆ ∪ 𝑧)) |
| 14 | 13 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧 ↔ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧)) |
| 15 | 14 | elrab 3692 |
. . . . . . . 8
⊢ (𝐵 ∈ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} ↔ (𝐵 ∈ (𝐴[,]𝐵) ∧ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧)) |
| 16 | 15 | simprbi 496 |
. . . . . . 7
⊢ (𝐵 ∈ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧) |
| 17 | 11, 16 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ (𝑢 ∈ 𝒫 𝐽 ∧ (𝐴[,]𝐵) ⊆ ∪ 𝑢)) → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧) |
| 18 | 17 | expr 456 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) ∧ 𝑢 ∈ 𝒫 𝐽) → ((𝐴[,]𝐵) ⊆ ∪ 𝑢 → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧)) |
| 19 | 18 | ralrimiva 3146 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ∀𝑢 ∈ 𝒫 𝐽((𝐴[,]𝐵) ⊆ ∪ 𝑢 → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧)) |
| 20 | | retop 24782 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
| 21 | 2, 20 | eqeltri 2837 |
. . . . 5
⊢ 𝐽 ∈ Top |
| 22 | | iccssre 13469 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 23 | 22 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐴[,]𝐵) ⊆ ℝ) |
| 24 | | uniretop 24783 |
. . . . . . 7
⊢ ℝ =
∪ (topGen‘ran (,)) |
| 25 | 2 | unieqi 4919 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ (topGen‘ran (,)) |
| 26 | 24, 25 | eqtr4i 2768 |
. . . . . 6
⊢ ℝ =
∪ 𝐽 |
| 27 | 26 | cmpsub 23408 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ (𝐴[,]𝐵) ⊆ ℝ) → ((𝐽 ↾t (𝐴[,]𝐵)) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((𝐴[,]𝐵) ⊆ ∪ 𝑢 → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧))) |
| 28 | 21, 23, 27 | sylancr 587 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → ((𝐽 ↾t (𝐴[,]𝐵)) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐽((𝐴[,]𝐵) ⊆ ∪ 𝑢 → ∃𝑧 ∈ (𝒫 𝑢 ∩ Fin)(𝐴[,]𝐵) ⊆ ∪ 𝑧))) |
| 29 | 19, 28 | mpbird 257 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐴 ≤ 𝐵) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ Comp) |
| 30 | | rexr 11307 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
| 31 | | rexr 11307 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ → 𝐵 ∈
ℝ*) |
| 32 | | icc0 13435 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
| 33 | 30, 31, 32 | syl2an 596 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴[,]𝐵) = ∅ ↔ 𝐵 < 𝐴)) |
| 34 | 33 | biimpar 477 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐴[,]𝐵) = ∅) |
| 35 | 34 | oveq2d 7447 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐽 ↾t (𝐴[,]𝐵)) = (𝐽 ↾t
∅)) |
| 36 | | rest0 23177 |
. . . . . 6
⊢ (𝐽 ∈ Top → (𝐽 ↾t ∅) =
{∅}) |
| 37 | 21, 36 | ax-mp 5 |
. . . . 5
⊢ (𝐽 ↾t ∅) =
{∅} |
| 38 | 35, 37 | eqtrdi 2793 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐽 ↾t (𝐴[,]𝐵)) = {∅}) |
| 39 | | 0cmp 23402 |
. . . 4
⊢ {∅}
∈ Comp |
| 40 | 38, 39 | eqeltrdi 2849 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 𝐵 < 𝐴) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ Comp) |
| 41 | | lelttric 11368 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ∨ 𝐵 < 𝐴)) |
| 42 | 29, 40, 41 | mpjaodan 961 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐽 ↾t (𝐴[,]𝐵)) ∈ Comp) |
| 43 | 1, 42 | eqeltrid 2845 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝑇 ∈ Comp) |