Step | Hyp | Ref
| Expression |
1 | | lmmbr.3 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
2 | | lmmbr.2 |
. . . . 5
⊢ 𝐽 = (MetOpen‘𝐷) |
3 | 2 | mopntopon 22244 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
5 | 4 | lmbr 21062 |
. 2
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)))) |
6 | | rpxr 11840 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
7 | 2 | blopn 22305 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑥) ∈ 𝐽) |
8 | 6, 7 | syl3an3 1361 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑥) ∈ 𝐽) |
9 | | blcntr 22218 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+) → 𝑃 ∈ (𝑃(ball‘𝐷)𝑥)) |
10 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑃(ball‘𝐷)𝑥) → (𝑃 ∈ 𝑢 ↔ 𝑃 ∈ (𝑃(ball‘𝐷)𝑥))) |
11 | | feq3 6028 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = (𝑃(ball‘𝐷)𝑥) → ((𝐹 ↾ 𝑦):𝑦⟶𝑢 ↔ (𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
12 | 11 | rexbidv 3052 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑃(ball‘𝐷)𝑥) → (∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢 ↔ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
13 | 10, 12 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑃(ball‘𝐷)𝑥) → ((𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) ↔ (𝑃 ∈ (𝑃(ball‘𝐷)𝑥) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) |
14 | 13 | rspcva 3307 |
. . . . . . . . . . . 12
⊢ (((𝑃(ball‘𝐷)𝑥) ∈ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) → (𝑃 ∈ (𝑃(ball‘𝐷)𝑥) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
15 | 14 | impancom 456 |
. . . . . . . . . . 11
⊢ (((𝑃(ball‘𝐷)𝑥) ∈ 𝐽 ∧ 𝑃 ∈ (𝑃(ball‘𝐷)𝑥)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
16 | 8, 9, 15 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
17 | 16 | 3expa 1265 |
. . . . . . . . 9
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
18 | 17 | adantlrl 756 |
. . . . . . . 8
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) ∧ 𝑥 ∈ ℝ+) →
(∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
19 | 18 | impancom 456 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) → (𝑥 ∈ ℝ+ →
∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
20 | 19 | ralrimiv 2965 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) → ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)) |
21 | 2 | mopni2 22298 |
. . . . . . . . . . 11
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽 ∧ 𝑃 ∈ 𝑢) → ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) |
22 | | r19.29 3072 |
. . . . . . . . . . . 12
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) → ∃𝑥 ∈ ℝ+ (∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢)) |
23 | | fss 6056 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) → (𝐹 ↾ 𝑦):𝑦⟶𝑢) |
24 | 23 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢ ((𝑃(ball‘𝐷)𝑥) ⊆ 𝑢 → ((𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) → (𝐹 ↾ 𝑦):𝑦⟶𝑢)) |
25 | 24 | reximdv 3016 |
. . . . . . . . . . . . . 14
⊢ ((𝑃(ball‘𝐷)𝑥) ⊆ 𝑢 → (∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) |
26 | 25 | impcom 446 |
. . . . . . . . . . . . 13
⊢
((∃𝑦 ∈
ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) |
27 | 26 | rexlimivw 3029 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
ℝ+ (∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ ∃𝑥 ∈ ℝ+ (𝑃(ball‘𝐷)𝑥) ⊆ 𝑢) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) |
29 | 21, 28 | sylan2 491 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) ∧ (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑢 ∈ 𝐽 ∧ 𝑃 ∈ 𝑢)) → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) |
30 | 29 | 3exp2 1285 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥) → (𝐷 ∈ (∞Met‘𝑋) → (𝑢 ∈ 𝐽 → (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)))) |
31 | 30 | impcom 446 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ∀𝑥 ∈ ℝ+
∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)) → (𝑢 ∈ 𝐽 → (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))) |
32 | 31 | adantlr 751 |
. . . . . . 7
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)) → (𝑢 ∈ 𝐽 → (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))) |
33 | 32 | ralrimiv 2965 |
. . . . . 6
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)) → ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) |
34 | 20, 33 | impbida 877 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋)) → (∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
35 | 34 | pm5.32da 673 |
. . . 4
⊢ (𝐷 ∈ (∞Met‘𝑋) → (((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) ↔ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) |
36 | | df-3an 1039 |
. . . 4
⊢ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) ↔ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋) ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢))) |
37 | | df-3an 1039 |
. . . 4
⊢ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)) ↔ ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))) |
38 | 35, 36, 37 | 3bitr4g 303 |
. . 3
⊢ (𝐷 ∈ (∞Met‘𝑋) → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) |
39 | 1, 38 | syl 17 |
. 2
⊢ (𝜑 → ((𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑢 ∈ 𝐽 (𝑃 ∈ 𝑢 → ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶𝑢)) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) |
40 | 5, 39 | bitrd 268 |
1
⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧
𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran
ℤ≥(𝐹
↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) |