| Step | Hyp | Ref
| Expression |
| 1 | | lebnum.c |
. . 3
⊢ (𝜑 → 𝐽 ∈ Comp) |
| 2 | | lebnum.s |
. . 3
⊢ (𝜑 → 𝑈 ⊆ 𝐽) |
| 3 | | lebnum.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
| 4 | | metxmet 24344 |
. . . . . 6
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 6 | | lebnum.j |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
| 7 | 6 | mopnuni 24451 |
. . . . 5
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
| 8 | 5, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 9 | | lebnum.u |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ 𝑈) |
| 10 | 8, 9 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ∪ 𝐽 =
∪ 𝑈) |
| 11 | | eqid 2737 |
. . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 12 | 11 | cmpcov 23397 |
. . 3
⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ ∪ 𝐽 = ∪
𝑈) → ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)∪ 𝐽 =
∪ 𝑤) |
| 13 | 1, 2, 10, 12 | syl3anc 1373 |
. 2
⊢ (𝜑 → ∃𝑤 ∈ (𝒫 𝑈 ∩ Fin)∪
𝐽 = ∪ 𝑤) |
| 14 | | 1rp 13038 |
. . . 4
⊢ 1 ∈
ℝ+ |
| 15 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ (𝒫 𝑈 ∩ Fin)) |
| 16 | 15 | elin1d 4204 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ 𝒫 𝑈) |
| 17 | 16 | elpwid 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ⊆ 𝑈) |
| 18 | 17 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑤 ⊆ 𝑈) |
| 19 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ 𝑤) |
| 20 | 18, 19 | sseldd 3984 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑋 ∈ 𝑈) |
| 21 | 5 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 22 | | simpr 484 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 23 | | rpxr 13044 |
. . . . . . . 8
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
| 24 | 14, 23 | mp1i 13 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → 1 ∈
ℝ*) |
| 25 | | blssm 24428 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 1 ∈ ℝ*) →
(𝑥(ball‘𝐷)1) ⊆ 𝑋) |
| 26 | 21, 22, 24, 25 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → (𝑥(ball‘𝐷)1) ⊆ 𝑋) |
| 27 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑢 = 𝑋 → ((𝑥(ball‘𝐷)1) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)1) ⊆ 𝑋)) |
| 28 | 27 | rspcev 3622 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑈 ∧ (𝑥(ball‘𝐷)1) ⊆ 𝑋) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
| 29 | 20, 26, 28 | syl2anc 584 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) ∧ 𝑥 ∈ 𝑋) → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
| 30 | 29 | ralrimiva 3146 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) |
| 31 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑑 = 1 → (𝑥(ball‘𝐷)𝑑) = (𝑥(ball‘𝐷)1)) |
| 32 | 31 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑑 = 1 → ((𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
| 33 | 32 | rexbidv 3179 |
. . . . . 6
⊢ (𝑑 = 1 → (∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
| 34 | 33 | ralbidv 3178 |
. . . . 5
⊢ (𝑑 = 1 → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 ↔ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢)) |
| 35 | 34 | rspcev 3622 |
. . . 4
⊢ ((1
∈ ℝ+ ∧ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)1) ⊆ 𝑢) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
| 36 | 14, 30, 35 | sylancr 587 |
. . 3
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
| 37 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝐷 ∈ (Met‘𝑋)) |
| 38 | 1 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝐽 ∈ Comp) |
| 39 | 17 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ⊆ 𝑈) |
| 40 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑈 ⊆ 𝐽) |
| 41 | 39, 40 | sstrd 3994 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ⊆ 𝐽) |
| 42 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑋 = ∪ 𝐽) |
| 43 | | simplrr 778 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∪ 𝐽 = ∪
𝑤) |
| 44 | 42, 43 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑋 = ∪ 𝑤) |
| 45 | 15 | elin2d 4205 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → 𝑤 ∈ Fin) |
| 46 | 45 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → 𝑤 ∈ Fin) |
| 47 | | simpr 484 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ¬ 𝑋 ∈ 𝑤) |
| 48 | | eqid 2737 |
. . . . 5
⊢ (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑤 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, < )) = (𝑦 ∈ 𝑋 ↦ Σ𝑘 ∈ 𝑤 inf(ran (𝑧 ∈ (𝑋 ∖ 𝑘) ↦ (𝑦𝐷𝑧)), ℝ*, <
)) |
| 49 | | eqid 2737 |
. . . . 5
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
| 50 | 6, 37, 38, 41, 44, 46, 47, 48, 49 | lebnumlem3 24995 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
| 51 | | ssrexv 4053 |
. . . . . . 7
⊢ (𝑤 ⊆ 𝑈 → (∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
| 52 | 39, 51 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
| 53 | 52 | ralimdv 3169 |
. . . . 5
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
| 54 | 53 | reximdv 3170 |
. . . 4
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → (∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑤 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢)) |
| 55 | 50, 54 | mpd 15 |
. . 3
⊢ (((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) ∧ ¬ 𝑋 ∈ 𝑤) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
| 56 | 36, 55 | pm2.61dan 813 |
. 2
⊢ ((𝜑 ∧ (𝑤 ∈ (𝒫 𝑈 ∩ Fin) ∧ ∪ 𝐽 =
∪ 𝑤)) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |
| 57 | 13, 56 | rexlimddv 3161 |
1
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝑋 ∃𝑢 ∈ 𝑈 (𝑥(ball‘𝐷)𝑑) ⊆ 𝑢) |