Step | Hyp | Ref
| Expression |
1 | | icccmp.9 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
2 | | icccmp.4 |
. . . . . . . 8
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} |
3 | | ssrab2 3908 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)(𝐴[,]𝑥) ⊆ ∪ 𝑧} ⊆ (𝐴[,]𝐵) |
4 | 2, 3 | eqsstri 3854 |
. . . . . . 7
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
5 | | icccmp.5 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | | icccmp.6 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
7 | | iccssre 12571 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
8 | 5, 6, 7 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
9 | 4, 8 | syl5ss 3832 |
. . . . . 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 23037 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
16 | 15 | simpld 490 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
17 | 16 | ne0d 4150 |
. . . . . 6
⊢ (𝜑 → 𝑆 ≠ ∅) |
18 | 15 | simprd 491 |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) |
19 | | brralrspcev 4948 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧
∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵) → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
20 | 6, 18, 19 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) |
21 | | suprcl 11341 |
. . . . . 6
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) → sup(𝑆, ℝ, < ) ∈
ℝ) |
22 | 9, 17, 20, 21 | syl3anc 1439 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
23 | | suprub 11342 |
. . . . . 6
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) ∧ 𝐴 ∈ 𝑆) → 𝐴 ≤ sup(𝑆, ℝ, < )) |
24 | 9, 17, 20, 16, 23 | syl31anc 1441 |
. . . . 5
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
25 | | suprleub 11347 |
. . . . . . 7
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑣 ∈ ℝ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑣) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
26 | 9, 17, 20, 6, 25 | syl31anc 1441 |
. . . . . 6
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝐵)) |
27 | 18, 26 | mpbird 249 |
. . . . 5
⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵) |
28 | | elicc2 12554 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(sup(𝑆, ℝ, < )
∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
29 | 5, 6, 28 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵) ↔ (sup(𝑆, ℝ, < ) ∈ ℝ ∧ 𝐴 ≤ sup(𝑆, ℝ, < ) ∧ sup(𝑆, ℝ, < ) ≤ 𝐵))) |
30 | 22, 24, 27, 29 | mpbir3and 1399 |
. . . 4
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ (𝐴[,]𝐵)) |
31 | 1, 30 | sseldd 3822 |
. . 3
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈ ∪ 𝑈) |
32 | | eluni2 4677 |
. . 3
⊢
(sup(𝑆, ℝ,
< ) ∈ ∪ 𝑈 ↔ ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
33 | 31, 32 | sylib 210 |
. 2
⊢ (𝜑 → ∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢) |
34 | 14 | sselda 3821 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → 𝑢 ∈ 𝐽) |
35 | 12 | rexmet 23006 |
. . . . . . 7
⊢ 𝐷 ∈
(∞Met‘ℝ) |
36 | | eqid 2778 |
. . . . . . . . . 10
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
37 | 12, 36 | tgioo 23011 |
. . . . . . . . 9
⊢
(topGen‘ran (,)) = (MetOpen‘𝐷) |
38 | 10, 37 | eqtri 2802 |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐷) |
39 | 38 | mopni2 22710 |
. . . . . . 7
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ 𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
40 | 35, 39 | mp3an1 1521 |
. . . . . 6
⊢ ((𝑢 ∈ 𝐽 ∧ sup(𝑆, ℝ, < ) ∈ 𝑢) → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢) |
41 | 40 | ex 403 |
. . . . 5
⊢ (𝑢 ∈ 𝐽 → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
42 | 34, 41 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → ∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) |
43 | 5 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ∈ ℝ) |
44 | 6 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ ℝ) |
45 | 13 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐴 ≤ 𝐵) |
46 | 14 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑈 ⊆ 𝐽) |
47 | 1 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (𝐴[,]𝐵) ⊆ ∪ 𝑈) |
48 | | simplr 759 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑢 ∈ 𝑈) |
49 | | simprl 761 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝑤 ∈ ℝ+) |
50 | | simprr 763 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → (sup(𝑆, ℝ, < )(ball‘𝐷)𝑤) ⊆ 𝑢) |
51 | | eqid 2778 |
. . . . . 6
⊢ sup(𝑆, ℝ, < ) = sup(𝑆, ℝ, <
) |
52 | | eqid 2778 |
. . . . . 6
⊢
if((sup(𝑆, ℝ,
< ) + (𝑤 / 2)) ≤
𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) = if((sup(𝑆, ℝ, < ) + (𝑤 / 2)) ≤ 𝐵, (sup(𝑆, ℝ, < ) + (𝑤 / 2)), 𝐵) |
53 | 10, 11, 12, 2, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52 | icccmplem2 23038 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑈) ∧ (𝑤 ∈ ℝ+ ∧ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢)) → 𝐵 ∈ 𝑆) |
54 | 53 | rexlimdvaa 3214 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (∃𝑤 ∈ ℝ+ (sup(𝑆, ℝ, <
)(ball‘𝐷)𝑤) ⊆ 𝑢 → 𝐵 ∈ 𝑆)) |
55 | 42, 54 | syld 47 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑈) → (sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
56 | 55 | rexlimdva 3213 |
. 2
⊢ (𝜑 → (∃𝑢 ∈ 𝑈 sup(𝑆, ℝ, < ) ∈ 𝑢 → 𝐵 ∈ 𝑆)) |
57 | 33, 56 | mpd 15 |
1
⊢ (𝜑 → 𝐵 ∈ 𝑆) |