Proof of Theorem ubthlem1
Step | Hyp | Ref
| Expression |
1 | | rzal 4025 |
. . . . . . . . 9
⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
2 | 1 | ralrimivw 2950 |
. . . . . . . 8
⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
3 | | rabid2 3096 |
. . . . . . . 8
⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
4 | 2, 3 | sylibr 223 |
. . . . . . 7
⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
5 | 4 | eqcomd 2616 |
. . . . . 6
⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋) |
6 | 5 | eleq1d 2672 |
. . . . 5
⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽))) |
7 | | iinrab 4518 |
. . . . . . 7
⊢ (𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
9 | | id 22 |
. . . . . . 7
⊢ (𝑇 ≠ ∅ → 𝑇 ≠ ∅) |
10 | | ubthlem.7 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
11 | 10 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
12 | | ubthlem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐷 = (IndMet‘𝑈) |
13 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(IndMet‘𝑊) =
(IndMet‘𝑊) |
14 | | ubthlem.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐽 = (MetOpen‘𝐷) |
15 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊)) |
16 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) |
17 | | ubthlem.5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑈 ∈ CBan |
18 | | bnnv 27106 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑈 ∈ CBan → 𝑈 ∈
NrmCVec) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑈 ∈ NrmCVec |
20 | | ubthlem.6 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑊 ∈ NrmCVec |
21 | 12, 13, 14, 15, 16, 19, 20 | blocn2 27047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊)))) |
22 | | ubth.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑋 = (BaseSet‘𝑈) |
23 | 22, 12 | cbncms 27105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) |
24 | 17, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐷 ∈ (CMet‘𝑋) |
25 | | cmetmet 22892 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
26 | | metxmet 21949 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
27 | 24, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐷 ∈ (∞Met‘𝑋) |
28 | 14 | mopntopon 22054 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐽 ∈ (TopOn‘𝑋) |
30 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
31 | 30, 13 | imsxmet 26931 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ NrmCVec →
(IndMet‘𝑊) ∈
(∞Met‘(BaseSet‘𝑊))) |
32 | 20, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) |
33 | 15 | mopntopon 22054 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈
(TopOn‘(BaseSet‘𝑊))) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)) |
35 | | iscncl 20883 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))) |
36 | 29, 34, 35 | mp2an 704 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
37 | 21, 36 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
38 | 11, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
39 | 38 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
40 | 39 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
41 | 40 | ffvelrnda 6267 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
42 | 41 | biantrurd 528 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥))) |
44 | 43 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
45 | 44 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
46 | 42, 45 | syl6bbr 277 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
47 | 46 | pm5.32da 671 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
48 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → (𝑡‘𝑧) = (𝑡‘𝑥)) |
49 | 48 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥))) |
50 | 49 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
51 | 50 | elrab 3331 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
52 | 51 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
53 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋) |
54 | | elpreima 6245 |
. . . . . . . . . . . 12
⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
55 | 40, 53, 54 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
56 | 47, 52, 55 | 3bitr4d 299 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
57 | 56 | eqrdv 2608 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
58 | | nnre 10904 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
59 | 58 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ) |
60 | 59 | rexrd 9968 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*) |
61 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
62 | 30, 61 | nvzcl 26873 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ NrmCVec →
(0vec‘𝑊)
∈ (BaseSet‘𝑊)) |
63 | 20, 62 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0vec‘𝑊) ∈ (BaseSet‘𝑊) |
64 | | ubth.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 =
(normCV‘𝑊) |
65 | 30, 61, 64, 13 | nvnd 26927 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
66 | 20, 65 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
67 | | xmetsym 21962 |
. . . . . . . . . . . . . . . . 17
⊢
(((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
68 | 32, 63, 67 | mp3an12 1406 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (BaseSet‘𝑊) →
((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
69 | 66, 68 | eqtr4d 2647 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦)) |
70 | 69 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘)) |
71 | 70 | rabbiia 3161 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘} |
72 | 15, 71 | blcld 22120 |
. . . . . . . . . . . 12
⊢
(((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
73 | 32, 63, 72 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℝ*
→ {𝑦 ∈
(BaseSet‘𝑊) ∣
(𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
74 | 60, 73 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
75 | 38 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)) |
76 | 75 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)) |
77 | | imaeq2 5381 |
. . . . . . . . . . . 12
⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
78 | 77 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → ((◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) ↔ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))) |
79 | 78 | rspcv 3278 |
. . . . . . . . . 10
⊢ ({𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊))) → (∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))) |
80 | 74, 76, 79 | sylc 63 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)) |
81 | 57, 80 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
82 | 81 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
83 | | iincld 20653 |
. . . . . . 7
⊢ ((𝑇 ≠ ∅ ∧
∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
84 | 9, 82, 83 | syl2anr 494 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
85 | 8, 84 | eqeltrrd 2689 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
86 | 14 | mopntop 22055 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
87 | 27, 86 | ax-mp 5 |
. . . . . . 7
⊢ 𝐽 ∈ Top |
88 | 29 | toponunii 20547 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
89 | 88 | topcld 20649 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽)) |
90 | 87, 89 | ax-mp 5 |
. . . . . 6
⊢ 𝑋 ∈ (Clsd‘𝐽) |
91 | 90 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽)) |
92 | 6, 85, 91 | pm2.61ne 2867 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
93 | | ubthlem.9 |
. . . 4
⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
94 | 92, 93 | fmptd 6292 |
. . 3
⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽)) |
95 | | frn 5966 |
. . . . . . 7
⊢ (𝐴:ℕ⟶(Clsd‘𝐽) → ran 𝐴 ⊆ (Clsd‘𝐽)) |
96 | 94, 95 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽)) |
97 | 88 | cldss2 20644 |
. . . . . 6
⊢
(Clsd‘𝐽)
⊆ 𝒫 𝑋 |
98 | 96, 97 | syl6ss 3580 |
. . . . 5
⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋) |
99 | | sspwuni 4547 |
. . . . 5
⊢ (ran
𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋) |
100 | 98, 99 | sylib 207 |
. . . 4
⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋) |
101 | | ubthlem.8 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
102 | | arch 11166 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℝ →
∃𝑘 ∈ ℕ
𝑐 < 𝑘) |
103 | 102 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘) |
104 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ) |
105 | | ltle 10005 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘)) |
106 | 104, 58, 105 | syl2an 493 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘)) |
107 | 106 | impr 647 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘) |
108 | 107 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘) |
109 | 39 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
110 | 109 | an32s 842 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
111 | 30, 64 | nvcl 26900 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
112 | 20, 110, 111 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
113 | 112 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
114 | 113 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
115 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ∈ ℝ) |
116 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℕ) |
117 | 116, 58 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ) |
118 | | letr 10010 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
119 | 114, 115,
117, 118 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
120 | 108, 119 | mpan2d 706 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
121 | 120 | ralimdva 2945 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
122 | 121 | expr 641 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
123 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . 19
⊢
(BaseSet‘𝑈)
∈ V |
124 | 22, 123 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 ∈ V |
125 | 124 | rabex 4740 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V |
126 | 93 | fvmpt2 6200 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
127 | 125, 126 | mpan2 703 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
128 | 127 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})) |
129 | 50 | ralbidv 2969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
130 | 129 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
131 | 128, 130 | syl6bb 275 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
132 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
133 | 132 | biantrurd 528 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
134 | 133 | bicomd 212 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
135 | 131, 134 | sylan9bbr 733 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
136 | | ffn 5958 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴:ℕ⟶(Clsd‘𝐽) → 𝐴 Fn ℕ) |
137 | 94, 136 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn ℕ) |
138 | 137 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ) |
139 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴) |
140 | | elssuni 4403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran
𝐴) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran
𝐴) |
142 | 141 | sseld 3567 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran
𝐴)) |
143 | 138, 142 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran
𝐴)) |
144 | 135, 143 | sylbird 249 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran
𝐴)) |
145 | 144 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran
𝐴)) |
146 | 122, 145 | syl6d 73 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴))) |
147 | 146 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴))) |
148 | 103, 147 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴)) |
149 | 148 | rexlimdva 3013 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴)) |
150 | 149 | ralimdva 2945 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴)) |
151 | 101, 150 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴) |
152 | | dfss3 3558 |
. . . . 5
⊢ (𝑋 ⊆ ∪ ran 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴) |
153 | 151, 152 | sylibr 223 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ∪ ran
𝐴) |
154 | 100, 153 | eqssd 3585 |
. . 3
⊢ (𝜑 → ∪ ran 𝐴 = 𝑋) |
155 | | eqid 2610 |
. . . . . 6
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
156 | 22, 155 | nvzcl 26873 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec →
(0vec‘𝑈)
∈ 𝑋) |
157 | | ne0i 3880 |
. . . . 5
⊢
((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅) |
158 | 19, 156, 157 | mp2b 10 |
. . . 4
⊢ 𝑋 ≠ ∅ |
159 | 14 | bcth2 22935 |
. . . 4
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
160 | 24, 158, 159 | mpanl12 714 |
. . 3
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
161 | 94, 154, 160 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
162 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽)) |
163 | 97, 162 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋) |
164 | 163 | elpwid 4118 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋) |
165 | 94, 164 | sylan 487 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋) |
166 | 88 | ntrss3 20674 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
167 | 87, 165, 166 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
168 | 167 | sseld 3567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋)) |
169 | 88 | ntropn 20663 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽) |
170 | 87, 165, 169 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽) |
171 | 14 | mopni2 22108 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
172 | 27, 171 | mp3an1 1403 |
. . . . . . . . 9
⊢
((((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
173 | 170, 172 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
174 | | elssuni 4403 |
. . . . . . . . . . . 12
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ ∪ 𝐽) |
175 | 174, 88 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
176 | 170, 175 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
177 | 176 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → 𝑦 ∈ 𝑋) |
178 | 88 | ntrss2 20671 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛)) |
179 | 87, 165, 178 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛)) |
180 | | sstr2 3575 |
. . . . . . . . . . . . 13
⊢ ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
181 | 179, 180 | syl5com 31 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
182 | 181 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
183 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
184 | 183, 27 | jctil 558 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋)) |
185 | | rphalfcl 11734 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
186 | 185 | rpxrd 11749 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ*) |
187 | | rpxr 11716 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
188 | | rphalflt 11736 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) < 𝑥) |
189 | 186, 187,
188 | 3jca 1235 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 / 2) ∈
ℝ* ∧ 𝑥
∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) |
190 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} |
191 | 14, 190 | blsscls2 22119 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ*
∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥)) |
192 | 184, 189,
191 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥)) |
193 | | sstr2 3575 |
. . . . . . . . . . . 12
⊢ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
194 | 192, 193 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
195 | 185 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
196 | | breq2 4587 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2))) |
197 | 196 | rabbidv 3164 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}) |
198 | 197 | sseq1d 3595 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
199 | 198 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢ (((𝑥 / 2) ∈ ℝ+
∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |
200 | 199 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 2) ∈ ℝ+
→ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
201 | 195, 200 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
202 | 182, 194,
201 | 3syld 58 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
203 | 202 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
204 | 177, 203 | syldan 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
205 | 173, 204 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |
206 | 205 | ex 449 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
207 | 168, 206 | jcad 554 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))) |
208 | 207 | eximdv 1833 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))) |
209 | | n0 3890 |
. . . 4
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) |
210 | | df-rex 2902 |
. . . 4
⊢
(∃𝑦 ∈
𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
211 | 208, 209,
210 | 3imtr4g 284 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
212 | 211 | reximdva 3000 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
213 | 161, 212 | mpd 15 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |