Step | Hyp | Ref
| Expression |
1 | | iscmet3.5 |
. . 3
⊢ (𝜑 → 𝐹 ∈ dom
(⇝𝑡‘𝐽)) |
2 | | eldmg 5319 |
. . . 4
⊢ (𝐹 ∈ dom
(⇝𝑡‘𝐽) → (𝐹 ∈ dom
(⇝𝑡‘𝐽) ↔ ∃𝑥 𝐹(⇝𝑡‘𝐽)𝑥)) |
3 | 2 | ibi 256 |
. . 3
⊢ (𝐹 ∈ dom
(⇝𝑡‘𝐽) → ∃𝑥 𝐹(⇝𝑡‘𝐽)𝑥) |
4 | 1, 3 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑥 𝐹(⇝𝑡‘𝐽)𝑥) |
5 | | iscmet3.4 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) |
6 | | metxmet 22139 |
. . . . . . 7
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
7 | 5, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
8 | | iscmet3.2 |
. . . . . . 7
⊢ 𝐽 = (MetOpen‘𝐷) |
9 | 8 | mopntopon 22244 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
10 | 7, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
11 | | lmcl 21101 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ 𝑋) |
12 | 10, 11 | sylan 488 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ 𝑋) |
13 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → 𝐷 ∈ (∞Met‘𝑋)) |
14 | 8 | mopni2 22298 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦) |
15 | 14 | 3expia 1267 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) |
16 | 13, 15 | sylan 488 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → ∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) |
17 | | iscmet3.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋)) |
18 | 17 | ad3antrrr 766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → 𝐺 ∈ (Fil‘𝑋)) |
19 | | iscmet3.3 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
20 | 19 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝑀 ∈
ℤ) |
21 | | rphalfcl 11858 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ℝ+
→ (𝑟 / 2) ∈
ℝ+) |
22 | 21 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ+) |
23 | | iscmet3.1 |
. . . . . . . . . . . 12
⊢ 𝑍 =
(ℤ≥‘𝑀) |
24 | 23 | iscmet3lem3 23088 |
. . . . . . . . . . 11
⊢ ((𝑀 ∈ ℤ ∧ (𝑟 / 2) ∈
ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < (𝑟 / 2)) |
25 | 20, 22, 24 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < (𝑟 / 2)) |
26 | 13 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐷 ∈ (∞Met‘𝑋)) |
27 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ 𝑋) |
28 | | blcntr 22218 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ+) →
𝑥 ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) |
29 | 26, 27, 22, 28 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝑥 ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) |
30 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹(⇝𝑡‘𝐽)𝑥) |
31 | 22 | rpxrd 11873 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑟 / 2) ∈
ℝ*) |
32 | 8 | blopn 22305 |
. . . . . . . . . . . 12
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ (𝑟 / 2) ∈ ℝ*) →
(𝑥(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
33 | 26, 27, 31, 32 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝐷)(𝑟 / 2)) ∈ 𝐽) |
34 | 23, 29, 20, 30, 33 | lmcvg 21066 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) →
∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) |
35 | 23 | rexanuz2 14089 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) ↔ (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < (𝑟 / 2) ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2)))) |
36 | 23 | r19.2uz 14091 |
. . . . . . . . . . . 12
⊢
(∃𝑗 ∈
𝑍 ∀𝑘 ∈
(ℤ≥‘𝑗)(((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → ∃𝑘 ∈ 𝑍 (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2)))) |
37 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → 𝐺 ∈ (Fil‘𝑋)) |
38 | | iscmet3.8 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆:ℤ⟶𝐺) |
39 | 38 | ad3antrrr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → 𝑆:ℤ⟶𝐺) |
40 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ ℤ) |
41 | 40, 23 | eleq2s 2719 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ) |
42 | 41 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → 𝑘 ∈ ℤ) |
43 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆:ℤ⟶𝐺 ∧ 𝑘 ∈ ℤ) → (𝑆‘𝑘) ∈ 𝐺) |
44 | 39, 42, 43 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → (𝑆‘𝑘) ∈ 𝐺) |
45 | | rpxr 11840 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
46 | 45 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
47 | | blssm 22223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ*) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑋) |
48 | 26, 27, 46, 47 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑋) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑋) |
50 | 41 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ ℤ) |
51 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℝ+ |
52 | | rphalfcl 11858 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (1 / 2)
∈ ℝ+ |
54 | | rpexpcl 12879 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((1 / 2)
∈ ℝ+ ∧ 𝑘 ∈ ℤ) → ((1 / 2)↑𝑘) ∈
ℝ+) |
55 | 53, 54 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℤ → ((1 /
2)↑𝑘) ∈
ℝ+) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈
ℝ+) |
57 | 56 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈ ℝ) |
58 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝑟 / 2) ∈
ℝ+) |
59 | 58 | rpred 11872 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝑟 / 2) ∈ ℝ) |
60 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((1 /
2)↑𝑘) ∈ ℝ
∧ (𝑟 / 2) ∈
ℝ) → (((1 / 2)↑𝑘) < (𝑟 / 2) → ((1 / 2)↑𝑘) ≤ (𝑟 / 2))) |
61 | 57, 59, 60 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((1 / 2)↑𝑘) < (𝑟 / 2) → ((1 / 2)↑𝑘) ≤ (𝑟 / 2))) |
62 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝜑) |
63 | | eluzfz2 12349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘)) |
64 | 63, 23 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ 𝑍 → 𝑘 ∈ (𝑀...𝑘)) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘)) |
66 | | iscmet3.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) |
67 | 66 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) |
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (𝑆‘𝑛) = (𝑆‘𝑘)) |
69 | 68 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → ((𝐹‘𝑘) ∈ (𝑆‘𝑛) ↔ (𝐹‘𝑘) ∈ (𝑆‘𝑘))) |
70 | 69 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ (𝑀...𝑘) → (∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛) → (𝐹‘𝑘) ∈ (𝑆‘𝑘))) |
71 | 65, 67, 70 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → (𝐹‘𝑘) ∈ (𝑆‘𝑘)) |
73 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → 𝑦 ∈ (𝑆‘𝑘)) |
74 | | iscmet3.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) |
76 | 41 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → 𝑘 ∈ ℤ) |
77 | | rsp 2929 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(∀𝑘 ∈
ℤ ∀𝑢 ∈
(𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘) → (𝑘 ∈ ℤ → ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))) |
78 | 75, 76, 77 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) |
79 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑢 = (𝐹‘𝑘) → (𝑢𝐷𝑣) = ((𝐹‘𝑘)𝐷𝑣)) |
80 | 79 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑢 = (𝐹‘𝑘) → ((𝑢𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹‘𝑘)𝐷𝑣) < ((1 / 2)↑𝑘))) |
81 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑣 = 𝑦 → ((𝐹‘𝑘)𝐷𝑣) = ((𝐹‘𝑘)𝐷𝑦)) |
82 | 81 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑦 → (((𝐹‘𝑘)𝐷𝑣) < ((1 / 2)↑𝑘) ↔ ((𝐹‘𝑘)𝐷𝑦) < ((1 / 2)↑𝑘))) |
83 | 80, 82 | rspc2va 3323 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐹‘𝑘) ∈ (𝑆‘𝑘) ∧ 𝑦 ∈ (𝑆‘𝑘)) ∧ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) → ((𝐹‘𝑘)𝐷𝑦) < ((1 / 2)↑𝑘)) |
84 | 72, 73, 78, 83 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → ((𝐹‘𝑘)𝐷𝑦) < ((1 / 2)↑𝑘)) |
85 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → 𝐷 ∈ (∞Met‘𝑋)) |
86 | 41, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑘 ∈ 𝑍 → ((1 / 2)↑𝑘) ∈
ℝ+) |
87 | 86 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ 𝑍 → ((1 / 2)↑𝑘) ∈
ℝ*) |
88 | 87 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → ((1 / 2)↑𝑘) ∈
ℝ*) |
89 | | iscmet3.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝐹:𝑍⟶𝑋) |
90 | 89 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑋) |
91 | 90 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → (𝐹‘𝑘) ∈ 𝑋) |
92 | 17 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐺 ∈ (Fil‘𝑋)) |
93 | 38, 41, 43 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑆‘𝑘) ∈ 𝐺) |
94 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺 ∈ (Fil‘𝑋) ∧ (𝑆‘𝑘) ∈ 𝐺) → (𝑆‘𝑘) ⊆ 𝑋) |
95 | 92, 93, 94 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑆‘𝑘) ⊆ 𝑋) |
96 | 95 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → 𝑦 ∈ 𝑋) |
97 | | elbl2 22195 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ ((1 / 2)↑𝑘) ∈ ℝ*)
∧ ((𝐹‘𝑘) ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑦 ∈ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ↔ ((𝐹‘𝑘)𝐷𝑦) < ((1 / 2)↑𝑘))) |
98 | 85, 88, 91, 96, 97 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → (𝑦 ∈ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ↔ ((𝐹‘𝑘)𝐷𝑦) < ((1 / 2)↑𝑘))) |
99 | 84, 98 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ 𝑦 ∈ (𝑆‘𝑘)) → 𝑦 ∈ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘))) |
100 | 99 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑦 ∈ (𝑆‘𝑘) → 𝑦 ∈ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)))) |
101 | 100 | ssrdv 3609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘))) |
102 | 62, 101 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘))) |
103 | 26 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝐷 ∈ (∞Met‘𝑋)) |
104 | 89 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑍⟶𝑋) |
105 | 104 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈ 𝑋) |
106 | 56 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((1 / 2)↑𝑘) ∈
ℝ*) |
107 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝑟 / 2) ∈
ℝ*) |
108 | | ssbl 22228 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ (((1 / 2)↑𝑘) ∈ ℝ* ∧ (𝑟 / 2) ∈
ℝ*) ∧ ((1 / 2)↑𝑘) ≤ (𝑟 / 2)) → ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2))) |
109 | 108 | 3expia 1267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ (((1 / 2)↑𝑘) ∈ ℝ* ∧ (𝑟 / 2) ∈
ℝ*)) → (((1 / 2)↑𝑘) ≤ (𝑟 / 2) → ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
110 | 103, 105,
106, 107, 109 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((1 / 2)↑𝑘) ≤ (𝑟 / 2) → ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
111 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ∧ ((𝐹‘𝑘)(ball‘𝐷)((1 / 2)↑𝑘)) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2))) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2))) |
112 | 102, 110,
111 | syl6an 568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((1 / 2)↑𝑘) ≤ (𝑟 / 2) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
113 | 61, 112 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (((1 / 2)↑𝑘) < (𝑟 / 2) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
114 | 113 | adantrd 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
115 | 114 | impr 649 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → (𝑆‘𝑘) ⊆ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2))) |
116 | 27 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝑥 ∈ 𝑋) |
117 | | blcom 22199 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑟 / 2) ∈ ℝ*) ∧
(𝑥 ∈ 𝑋 ∧ (𝐹‘𝑘) ∈ 𝑋)) → ((𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2)) ↔ 𝑥 ∈ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
118 | 103, 107,
116, 105, 117 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2)) ↔ 𝑥 ∈ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) |
119 | | rpre 11839 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ) |
120 | 119 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → 𝑟 ∈ ℝ) |
121 | | blhalf 22210 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ (𝑟 ∈ ℝ ∧ 𝑥 ∈ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)))) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟)) |
122 | 121 | expr 643 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ (𝐹‘𝑘) ∈ 𝑋) ∧ 𝑟 ∈ ℝ) → (𝑥 ∈ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟))) |
123 | 103, 105,
120, 122 | syl21anc 1325 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → (𝑥 ∈ ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟))) |
124 | 118, 123 | sylbid 230 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2)) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟))) |
125 | 124 | adantld 483 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ 𝑘 ∈ 𝑍) → ((((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟))) |
126 | 125 | impr 649 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → ((𝐹‘𝑘)(ball‘𝐷)(𝑟 / 2)) ⊆ (𝑥(ball‘𝐷)𝑟)) |
127 | 115, 126 | sstrd 3613 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → (𝑆‘𝑘) ⊆ (𝑥(ball‘𝐷)𝑟)) |
128 | | filss 21657 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ (Fil‘𝑋) ∧ ((𝑆‘𝑘) ∈ 𝐺 ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑋 ∧ (𝑆‘𝑘) ⊆ (𝑥(ball‘𝐷)𝑟))) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺) |
129 | 37, 44, 49, 127, 128 | syl13anc 1328 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ 𝑍 ∧ (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))))) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺) |
130 | 129 | rexlimdvaa 3032 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) →
(∃𝑘 ∈ 𝑍 (((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺)) |
131 | 36, 130 | syl5 34 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(((1 / 2)↑𝑘) < (𝑟 / 2) ∧ (𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺)) |
132 | 35, 131 | syl5bir 233 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) →
((∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < (𝑟 / 2) ∧ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ (𝑥(ball‘𝐷)(𝑟 / 2))) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺)) |
133 | 25, 34, 132 | mp2and 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑟 ∈ ℝ+) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺) |
134 | 133 | ad2ant2r 783 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → (𝑥(ball‘𝐷)𝑟) ∈ 𝐺) |
135 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → 𝐽 ∈ (TopOn‘𝑋)) |
136 | | toponss 20731 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑦 ∈ 𝐽) → 𝑦 ⊆ 𝑋) |
137 | 135, 136 | sylan 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) → 𝑦 ⊆ 𝑋) |
138 | 137 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → 𝑦 ⊆ 𝑋) |
139 | | simprr 796 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦) |
140 | | filss 21657 |
. . . . . . . 8
⊢ ((𝐺 ∈ (Fil‘𝑋) ∧ ((𝑥(ball‘𝐷)𝑟) ∈ 𝐺 ∧ 𝑦 ⊆ 𝑋 ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → 𝑦 ∈ 𝐺) |
141 | 18, 134, 138, 139, 140 | syl13anc 1328 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) ∧ (𝑟 ∈ ℝ+ ∧ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦)) → 𝑦 ∈ 𝐺) |
142 | 141 | rexlimdvaa 3032 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) → (∃𝑟 ∈ ℝ+ (𝑥(ball‘𝐷)𝑟) ⊆ 𝑦 → 𝑦 ∈ 𝐺)) |
143 | 16, 142 | syld 47 |
. . . . 5
⊢ (((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺)) |
144 | 143 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺)) |
145 | | flimopn 21779 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐺) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺)))) |
146 | 10, 17, 145 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐺) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺)))) |
147 | 146 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → (𝑥 ∈ (𝐽 fLim 𝐺) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐺)))) |
148 | 12, 144, 147 | mpbir2and 957 |
. . 3
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ (𝐽 fLim 𝐺)) |
149 | | ne0i 3921 |
. . 3
⊢ (𝑥 ∈ (𝐽 fLim 𝐺) → (𝐽 fLim 𝐺) ≠ ∅) |
150 | 148, 149 | syl 17 |
. 2
⊢ ((𝜑 ∧ 𝐹(⇝𝑡‘𝐽)𝑥) → (𝐽 fLim 𝐺) ≠ ∅) |
151 | 4, 150 | exlimddv 1863 |
1
⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅) |