Step | Hyp | Ref
| Expression |
1 | | lebnum.c |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
2 | | lebnum.s |
. . 3
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
3 | | lebnum.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
4 | | metxmet 22551 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
6 | | lebnum.j |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
7 | 6 | mopnuni 22658 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
8 | 5, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
9 | | lebnum.u |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝑈) |
10 | 8, 9 | eqtr3d 2816 |
. . 3
⊢ (𝜑 → ∪ 𝐽 =
∪ 𝑈) |
11 | | eqid 2778 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
12 | 11 | cmpcov 21605 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈) → ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑤) |
13 | 1, 2, 10, 12 | syl3anc 1439 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)∪
𝐽 = ∪ 𝑤) |
14 | | 1rp 12145 |
. . . 4
⊢ 1 ∈
ℝ+ |
15 | | inss1 4053 |
. . . . . . . . . 10
⊢
(𝒫 𝑈 ∩
Fin) ⊆ 𝒫 𝑈 |
16 | | simprl 761 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ (𝒫 𝑈 ∩ Fin)) |
17 | 15, 16 | sseldi 3819 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ 𝒫 𝑈) |
18 | 17 | elpwid 4391 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ⊆ 𝑈) |
19 | 18 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑤 ⊆ 𝑈) |
20 | | simplr 759 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ 𝑤) |
21 | 19, 20 | sseldd 3822 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ 𝑈) |
22 | 5 | ad3antrrr 720 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
23 | | simpr 479 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
24 | | rpxr 12152 |
. . . . . . . 8
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
25 | 14, 24 | mp1i 13 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 1 ∈
ℝ*) |
26 | | blssm 22635 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ*) →
(𝑥(ball‘𝐷)1) ⊆ 𝑋) |
27 | 22, 23, 25, 26 | syl3anc 1439 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝐷)1) ⊆ 𝑋) |
28 | | sseq2 3846 |
. . . . . . 7
⊢ (𝑢 = 𝑋 → ((𝑥(ball‘𝐷)1) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)1) ⊆ 𝑋)) |
29 | 28 | rspcev 3511 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ (𝑥(ball‘𝐷)1) ⊆ 𝑋) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
30 | 21, 27, 29 | syl2anc 579 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
31 | 30 | ralrimiva 3148 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
32 | | oveq2 6932 |
. . . . . . . 8
⊢ (𝑑 = 1 → (𝑥(ball‘𝐷)𝑑) = (𝑥(ball‘𝐷)1)) |
33 | 32 | sseq1d 3851 |
. . . . . . 7
⊢ (𝑑 = 1 → ((𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
34 | 33 | rexbidv 3237 |
. . . . . 6
⊢ (𝑑 = 1 → (∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
35 | 34 | ralbidv 3168 |
. . . . 5
⊢ (𝑑 = 1 → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
36 | 35 | rspcev 3511 |
. . . 4
⊢ ((1
∈ ℝ+ ∧ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
37 | 14, 31, 36 | sylancr 581 |
. . 3
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
38 | 3 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝐷 ∈ (Met‘𝑋)) |
39 | 1 | ad2antrr 716 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝐽 ∈ Comp) |
40 | 18 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ⊆ 𝑈) |
41 | 2 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑈 ⊆ 𝐽) |
42 | 40, 41 | sstrd 3831 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ⊆ 𝐽) |
43 | 8 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑋 = ∪ 𝐽) |
44 | | simplrr 768 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∪ 𝐽 = ∪
𝑤) |
45 | 43, 44 | eqtrd 2814 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑋 = ∪ 𝑤) |
46 | | inss2 4054 |
. . . . . . 7
⊢
(𝒫 𝑈 ∩
Fin) ⊆ Fin |
47 | 46, 16 | sseldi 3819 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ Fin) |
48 | 47 | adantr 474 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ∈ Fin) |
49 | | simpr 479 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ¬ 𝑋 ∈ 𝑤) |
50 | | eqid 2778 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑤 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑤 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) |
51 | | eqid 2778 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
52 | 6, 38, 39, 42, 45, 48, 49, 50, 51 | lebnumlem3 23174 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
53 | | ssrexv 3886 |
. . . . . . 7
⊢ (𝑤 ⊆ 𝑈 → (∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
54 | 40, 53 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
55 | 54 | ralimdv 3145 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
56 | 55 | reximdv 3197 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
57 | 52, 56 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
58 | 37, 57 | pm2.61dan 803 |
. 2
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
59 | 13, 58 | rexlimddv 3218 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |