Step | Hyp | Ref
| Expression |
1 | | icccmp.9 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
2 | | icccmp.4 |
. . . . . . . 8
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
3 | | ssrab2 3687 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} ⊆ (𝐴[,]𝐵) |
4 | 2, 3 | eqsstri 3635 |
. . . . . . 7
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
5 | | icccmp.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | icccmp.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | iccssre 12255 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 5, 6, 7 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
9 | 4, 8 | syl5ss 3614 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
10 | | icccmp.1 |
. . . . . . . . 9
⊢ 𝐽 = (topGen‘ran
(,)) |
11 | | icccmp.2 |
. . . . . . . . 9
⊢ 𝑇 = (𝐽 ↾t (𝐴[,]𝐵)) |
12 | | icccmp.3 |
. . . . . . . . 9
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
13 | | icccmp.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
14 | | icccmp.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
15 | 10, 11, 12, 2, 5, 6,
13, 14, 1 | icccmplem1 22625 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
16 | 15 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
17 | | ne0i 3921 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑆 → 𝑆 ≠ ∅) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ ∅) |
19 | 15 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
20 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑣 = 𝐵 → (𝑦 ≤ 𝑣 ↔ 𝑦 ≤ 𝐵)) |
21 | 20 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑣 = 𝐵 → (∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
22 | 21 | rspcev 3309 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
23 | 6, 19, 22 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
24 | | suprcl 10983 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) → sup(𝑆, ℝ, < ) ∈
ℝ) |
25 | 9, 18, 23, 24 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
26 | | suprub 10984 |
. . . . . 6
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) ∧ 𝐴 ∈ 𝑆) → 𝐴 ≤ sup(𝑆, ℝ, < )) |
27 | 9, 18, 23, 16, 26 | syl31anc 1329 |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
28 | | suprleub 10989 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
29 | 9, 18, 23, 6, 28 | syl31anc 1329 |
. . . . . 6
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
30 | 19, 29 | mpbird 247 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵) |
31 | | elicc2 12238 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(sup(𝑆, ℝ, < )
∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
32 | 5, 6, 31 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
33 | 25, 27, 30, 32 | mpbir3and 1245 |
. . . 4
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵)) |
34 | 1, 33 | sseldd 3604 |
. . 3
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ∪ 𝑈) |
35 | | eluni2 4440 |
. . 3
⊢
(sup(𝑆, ℝ,
< ) ∈ ∪ 𝑈 ↔ ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
36 | 34, 35 | sylib 208 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
37 | 14 | sselda 3603 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐽) |
38 | 12 | rexmet 22594 |
. . . . . . 7
⊢ 𝐷 ∈
(∞Met‘ℝ) |
39 | | eqid 2622 |
. . . . . . . . . 10
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
40 | 12, 39 | tgioo 22599 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘𝐷) |
41 | 10, 40 | eqtri 2644 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐷) |
42 | 41 | mopni2 22298 |
. . . . . . 7
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
43 | 38, 42 | mp3an1 1411 |
. . . . . 6
⊢ ((𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
44 | 43 | ex 450 |
. . . . 5
⊢ (𝑢 ∈ 𝐽 → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
45 | 37, 44 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
46 | 5 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ∈ ℝ) |
47 | 6 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ ℝ) |
48 | 13 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ≤ 𝐵) |
49 | 14 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑈 ⊆ 𝐽) |
50 | 1 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
51 | | simplr 792 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑢 ∈ 𝑈) |
52 | | simprl 794 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑤 ∈ ℝ+) |
53 | | simprr 796 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (sup(𝑆, ℝ, < )(ball‘𝐷)𝑤) ⊆ 𝑢) |
54 | | eqid 2622 |
. . . . . 6
⊢ sup(𝑆, ℝ, < ) = sup(𝑆, ℝ, <
) |
55 | | eqid 2622 |
. . . . . 6
⊢
if((sup(𝑆, ℝ,
< ) + (𝑤 / 2)) ≤
𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) = if((sup(𝑆, ℝ, < ) + (𝑤 / 2)) ≤ 𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) |
56 | 10, 11, 12, 2, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55 | icccmplem2 22626 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ 𝑆) |
57 | 56 | rexlimdvaa 3032 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢 → 𝐵 ∈ 𝑆)) |
58 | 45, 57 | syld 47 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
59 | 58 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
60 | 36, 59 | mpd 15 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |