| Step | Hyp | Ref
| Expression |
| 1 | | icccmp.9 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
| 2 | | icccmp.4 |
. . . . . . . 8
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
| 3 | 2 | ssrab3 4082 |
. . . . . . 7
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
| 4 | | icccmp.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 5 | | icccmp.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 6 | | iccssre 13469 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
| 7 | 4, 5, 6 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
| 8 | 3, 7 | sstrid 3995 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
| 9 | | icccmp.1 |
. . . . . . . . 9
⊢ 𝐽 = (topGen‘ran
(,)) |
| 10 | | icccmp.2 |
. . . . . . . . 9
⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) |
| 11 | | icccmp.3 |
. . . . . . . . 9
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
| 12 | | icccmp.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 13 | | icccmp.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
| 14 | 9, 10, 11, 2, 4, 5,
12, 13, 1 | icccmplem1 24844 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
| 15 | 14 | simpld 494 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
| 16 | 15 | ne0d 4342 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ ∅) |
| 17 | 14 | simprd 495 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
| 18 | | brralrspcev 5203 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
| 19 | 5, 17, 18 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
| 20 | 8, 16, 19 | suprcld 12231 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
| 21 | 8, 16, 19, 15 | suprubd 12230 |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
| 22 | | suprleub 12234 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
| 23 | 8, 16, 19, 5, 22 | syl31anc 1375 |
. . . . . 6
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
| 24 | 17, 23 | mpbird 257 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵) |
| 25 | | elicc2 13452 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(sup(𝑆, ℝ, < )
∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
| 26 | 4, 5, 25 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
| 27 | 20, 21, 24, 26 | mpbir3and 1343 |
. . . 4
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵)) |
| 28 | 1, 27 | sseldd 3984 |
. . 3
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ∪ 𝑈) |
| 29 | | eluni2 4911 |
. . 3
⊢
(sup(𝑆, ℝ,
< ) ∈ ∪ 𝑈 ↔ ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
| 30 | 28, 29 | sylib 218 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
| 31 | 13 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐽) |
| 32 | 11 | rexmet 24812 |
. . . . . . 7
⊢ 𝐷 ∈
(∞Met‘ℝ) |
| 33 | | eqid 2737 |
. . . . . . . . . 10
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
| 34 | 11, 33 | tgioo 24817 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘𝐷) |
| 35 | 9, 34 | eqtri 2765 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐷) |
| 36 | 35 | mopni2 24506 |
. . . . . . 7
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
| 37 | 32, 36 | mp3an1 1450 |
. . . . . 6
⊢ ((𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
| 38 | 37 | ex 412 |
. . . . 5
⊢ (𝑢 ∈ 𝐽 → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
| 39 | 31, 38 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
| 40 | 4 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ∈ ℝ) |
| 41 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ ℝ) |
| 42 | 12 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ≤ 𝐵) |
| 43 | 13 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑈 ⊆ 𝐽) |
| 44 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
| 45 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑢 ∈ 𝑈) |
| 46 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑤 ∈ ℝ+) |
| 47 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (sup(𝑆, ℝ, < )(ball‘𝐷)𝑤) ⊆ 𝑢) |
| 48 | | eqid 2737 |
. . . . . 6
⊢ sup(𝑆, ℝ, < ) = sup(𝑆, ℝ, <
) |
| 49 | | eqid 2737 |
. . . . . 6
⊢
if((sup(𝑆, ℝ,
< ) + (𝑤 / 2)) ≤
𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) = if((sup(𝑆, ℝ, < ) + (𝑤 / 2)) ≤ 𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) |
| 50 | 9, 10, 11, 2, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49 | icccmplem2 24845 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ 𝑆) |
| 51 | 50 | rexlimdvaa 3156 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢 → 𝐵 ∈ 𝑆)) |
| 52 | 39, 51 | syld 47 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
| 53 | 52 | rexlimdva 3155 |
. 2
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
| 54 | 30, 53 | mpd 15 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |