Proof of Theorem ubthlem1
| Step | Hyp | Ref
| Expression |
| 1 | | rzal 4509 |
. . . . . . . . 9
⊢ (𝑇 = ∅ → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
| 2 | 1 | ralrimivw 3150 |
. . . . . . . 8
⊢ (𝑇 = ∅ → ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
| 3 | | rabid2 3470 |
. . . . . . . 8
⊢ (𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ ∀𝑧 ∈ 𝑋 ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘) |
| 4 | 2, 3 | sylibr 234 |
. . . . . . 7
⊢ (𝑇 = ∅ → 𝑋 = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 5 | 4 | eqcomd 2743 |
. . . . . 6
⊢ (𝑇 = ∅ → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = 𝑋) |
| 6 | 5 | eleq1d 2826 |
. . . . 5
⊢ (𝑇 = ∅ → ({𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽))) |
| 7 | | iinrab 5069 |
. . . . . . 7
⊢ (𝑇 ≠ ∅ → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 8 | 7 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 9 | | id 22 |
. . . . . . 7
⊢ (𝑇 ≠ ∅ → 𝑇 ≠ ∅) |
| 10 | | ubthlem.7 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
| 11 | 10 | sselda 3983 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
| 12 | | ubthlem.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐷 = (IndMet‘𝑈) |
| 13 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(IndMet‘𝑊) =
(IndMet‘𝑊) |
| 14 | | ubthlem.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐽 = (MetOpen‘𝐷) |
| 15 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(MetOpen‘(IndMet‘𝑊)) = (MetOpen‘(IndMet‘𝑊)) |
| 16 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) |
| 17 | | ubthlem.5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑈 ∈ CBan |
| 18 | | bnnv 30885 |
. . . . . . . . . . . . . . . . . . . . 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 30827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊)))) |
| 22 | | ubth.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑋 = (BaseSet‘𝑈) |
| 23 | 22, 12 | cbncms 30884 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) |
| 24 | 17, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝐷 ∈ (CMet‘𝑋) |
| 25 | | cmetmet 25320 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) |
| 26 | | metxmet 24344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋)) |
| 27 | 24, 25, 26 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐷 ∈ (∞Met‘𝑋) |
| 28 | 14 | mopntopon 24449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
| 29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐽 ∈ (TopOn‘𝑋) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 31 | 30, 13 | imsxmet 30711 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑊 ∈ NrmCVec →
(IndMet‘𝑊) ∈
(∞Met‘(BaseSet‘𝑊))) |
| 32 | 20, 31 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) |
| 33 | 15 | mopntopon 24449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈
(TopOn‘(BaseSet‘𝑊))) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)) |
| 35 | | iscncl 23277 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧
(MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)))) |
| 36 | 29, 34, 35 | mp2an 692 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
| 37 | 21, 36 | sylib 218 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
| 38 | 11, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽))) |
| 39 | 38 | simpld 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
| 40 | 39 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
| 41 | 40 | ffvelcdmda 7104 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
| 42 | 41 | biantrurd 532 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
| 43 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑡‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑡‘𝑥))) |
| 44 | 43 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑡‘𝑥) → ((𝑁‘𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 45 | 44 | elrab 3692 |
. . . . . . . . . . . . 13
⊢ ((𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ↔ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 46 | 42, 45 | bitr4di 289 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
| 47 | 46 | pm5.32da 579 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ((𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
| 48 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥))) |
| 49 | 48 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 50 | 49 | elrab 3692 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 51 | 50 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
| 52 | | ffn 6736 |
. . . . . . . . . . . 12
⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋) |
| 53 | | elpreima 7078 |
. . . . . . . . . . . 12
⊢ (𝑡 Fn 𝑋 → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
| 54 | 40, 52, 53 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ↔ (𝑥 ∈ 𝑋 ∧ (𝑡‘𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
| 55 | 47, 51, 54 | 3bitr4d 311 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}))) |
| 56 | 55 | eqrdv 2735 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
| 57 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → (◡𝑡 “ 𝑥) = (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘})) |
| 58 | 57 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} → ((◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽) ↔ (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))) |
| 59 | 38 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)) |
| 60 | 59 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → ∀𝑥 ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))(◡𝑡 “ 𝑥) ∈ (Clsd‘𝐽)) |
| 61 | | nnre 12273 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 62 | 61 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ) |
| 63 | 62 | rexrd 11311 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ*) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
| 65 | 30, 64 | nvzcl 30653 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ NrmCVec →
(0vec‘𝑊)
∈ (BaseSet‘𝑊)) |
| 66 | 20, 65 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(0vec‘𝑊) ∈ (BaseSet‘𝑊) |
| 67 | | ubth.2 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑁 =
(normCV‘𝑊) |
| 68 | 30, 64, 67, 13 | nvnd 30707 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
| 69 | 20, 68 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
| 70 | | xmetsym 24357 |
. . . . . . . . . . . . . . . . 17
⊢
(((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
| 71 | 32, 66, 70 | mp3an12 1453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (BaseSet‘𝑊) →
((0vec‘𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec‘𝑊))) |
| 72 | 69, 71 | eqtr4d 2780 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (BaseSet‘𝑊) → (𝑁‘𝑦) = ((0vec‘𝑊)(IndMet‘𝑊)𝑦)) |
| 73 | 72 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁‘𝑦) ≤ 𝑘 ↔ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘)) |
| 74 | 73 | rabbiia 3440 |
. . . . . . . . . . . . 13
⊢ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec‘𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘} |
| 75 | 15, 74 | blcld 24518 |
. . . . . . . . . . . 12
⊢
(((IndMet‘𝑊)
∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
| 76 | 32, 66, 75 | mp3an12 1453 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℝ*
→ {𝑦 ∈
(BaseSet‘𝑊) ∣
(𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
| 77 | 63, 76 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘} ∈
(Clsd‘(MetOpen‘(IndMet‘𝑊)))) |
| 78 | 58, 60, 77 | rspcdva 3623 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → (◡𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁‘𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)) |
| 79 | 56, 78 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑡 ∈ 𝑇) → {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 80 | 79 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 81 | | iincld 23047 |
. . . . . . 7
⊢ ((𝑇 ≠ ∅ ∧
∀𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 82 | 9, 80, 81 | syl2anr 597 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → ∩ 𝑡 ∈ 𝑇 {𝑧 ∈ 𝑋 ∣ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 83 | 8, 82 | eqeltrrd 2842 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 84 | 14 | mopntop 24450 |
. . . . . . . 8
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
| 85 | 27, 84 | ax-mp 5 |
. . . . . . 7
⊢ 𝐽 ∈ Top |
| 86 | 29 | toponunii 22922 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
| 87 | 86 | topcld 23043 |
. . . . . . 7
⊢ (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽)) |
| 88 | 85, 87 | ax-mp 5 |
. . . . . 6
⊢ 𝑋 ∈ (Clsd‘𝐽) |
| 89 | 88 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽)) |
| 90 | 6, 83, 89 | pm2.61ne 3027 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) |
| 91 | | ubthlem.9 |
. . . 4
⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 92 | 90, 91 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐴:ℕ⟶(Clsd‘𝐽)) |
| 93 | 92 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽)) |
| 94 | 86 | cldss2 23038 |
. . . . . 6
⊢
(Clsd‘𝐽)
⊆ 𝒫 𝑋 |
| 95 | 93, 94 | sstrdi 3996 |
. . . . 5
⊢ (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋) |
| 96 | | sspwuni 5100 |
. . . . 5
⊢ (ran
𝐴 ⊆ 𝒫 𝑋 ↔ ∪ ran 𝐴 ⊆ 𝑋) |
| 97 | 95, 96 | sylib 218 |
. . . 4
⊢ (𝜑 → ∪ ran 𝐴 ⊆ 𝑋) |
| 98 | | ubthlem.8 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
| 99 | | arch 12523 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ℝ →
∃𝑘 ∈ ℕ
𝑐 < 𝑘) |
| 100 | 99 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘) |
| 101 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ) |
| 102 | | ltle 11349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘)) |
| 103 | 101, 61, 102 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → 𝑐 ≤ 𝑘)) |
| 104 | 103 | impr 454 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐 ≤ 𝑘) |
| 105 | 104 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ≤ 𝑘) |
| 106 | 39 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑥 ∈ 𝑋) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
| 107 | 106 | an32s 652 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
| 108 | 30, 67 | nvcl 30680 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
| 109 | 20, 107, 108 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
| 110 | 109 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
| 111 | 110 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
| 112 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑐 ∈ ℝ) |
| 113 | | simplrl 777 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℕ) |
| 114 | 113, 61 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → 𝑘 ∈ ℝ) |
| 115 | | letr 11355 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁‘(𝑡‘𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 116 | 111, 112,
114, 115 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → (((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ∧ 𝑐 ≤ 𝑘) → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 117 | 105, 116 | mpan2d 694 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡 ∈ 𝑇) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 118 | 117 | ralimdva 3167 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 119 | 118 | expr 456 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
| 120 | 22 | fvexi 6920 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑋 ∈ V |
| 121 | 120 | rabex 5339 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V |
| 122 | 91 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ ∧ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ∈ V) → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 123 | 121, 122 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → (𝐴‘𝑘) = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
| 124 | 123 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ 𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘})) |
| 125 | 49 | ralbidv 3178 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑥 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 126 | 125 | elrab 3692 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘} ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 127 | 124, 126 | bitrdi 287 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴‘𝑘) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
| 128 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
| 129 | 128 | biantrurd 532 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘))) |
| 130 | 129 | bicomd 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 ∈ 𝑋 ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 131 | 127, 130 | sylan9bbr 510 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘)) |
| 132 | 92 | ffnd 6737 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 Fn ℕ) |
| 133 | 132 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 Fn ℕ) |
| 134 | | fnfvelrn 7100 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ∈ ran 𝐴) |
| 135 | | elssuni 4937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘𝑘) ∈ ran 𝐴 → (𝐴‘𝑘) ⊆ ∪ ran
𝐴) |
| 136 | 134, 135 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴‘𝑘) ⊆ ∪ ran
𝐴) |
| 137 | 136 | sseld 3982 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran
𝐴)) |
| 138 | 133, 137 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴‘𝑘) → 𝑥 ∈ ∪ ran
𝐴)) |
| 139 | 131, 138 | sylbird 260 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran
𝐴)) |
| 140 | 139 | adantlr 715 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑘 → 𝑥 ∈ ∪ ran
𝐴)) |
| 141 | 119, 140 | syl6d 75 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴))) |
| 142 | 141 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴))) |
| 143 | 100, 142 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴)) |
| 144 | 143 | rexlimdva 3155 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → 𝑥 ∈ ∪ ran
𝐴)) |
| 145 | 144 | ralimdva 3167 |
. . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴)) |
| 146 | 98, 145 | mpd 15 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴) |
| 147 | | dfss3 3972 |
. . . . 5
⊢ (𝑋 ⊆ ∪ ran 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝑥 ∈ ∪ ran
𝐴) |
| 148 | 146, 147 | sylibr 234 |
. . . 4
⊢ (𝜑 → 𝑋 ⊆ ∪ ran
𝐴) |
| 149 | 97, 148 | eqssd 4001 |
. . 3
⊢ (𝜑 → ∪ ran 𝐴 = 𝑋) |
| 150 | | eqid 2737 |
. . . . . 6
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
| 151 | 22, 150 | nvzcl 30653 |
. . . . 5
⊢ (𝑈 ∈ NrmCVec →
(0vec‘𝑈)
∈ 𝑋) |
| 152 | | ne0i 4341 |
. . . . 5
⊢
((0vec‘𝑈) ∈ 𝑋 → 𝑋 ≠ ∅) |
| 153 | 19, 151, 152 | mp2b 10 |
. . . 4
⊢ 𝑋 ≠ ∅ |
| 154 | 14 | bcth2 25364 |
. . . 4
⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
| 155 | 24, 153, 154 | mpanl12 702 |
. . 3
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
| 156 | 92, 149, 155 | syl2anc 584 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅) |
| 157 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ (Clsd‘𝐽)) |
| 158 | 94, 157 | sselid 3981 |
. . . . . . . . . 10
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ∈ 𝒫 𝑋) |
| 159 | 158 | elpwid 4609 |
. . . . . . . . 9
⊢ ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋) |
| 160 | 92, 159 | sylan 580 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐴‘𝑛) ⊆ 𝑋) |
| 161 | 86 | ntrss3 23068 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
| 162 | 85, 160, 161 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
| 163 | 162 | sseld 3982 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → 𝑦 ∈ 𝑋)) |
| 164 | 86 | ntropn 23057 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽) |
| 165 | 85, 160, 164 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽) |
| 166 | 14 | mopni2 24506 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
| 167 | 27, 166 | mp3an1 1450 |
. . . . . . . . 9
⊢
((((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
| 168 | 165, 167 | sylan 580 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛))) |
| 169 | | elssuni 4937 |
. . . . . . . . . . . 12
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ ∪ 𝐽) |
| 170 | 169, 86 | sseqtrrdi 4025 |
. . . . . . . . . . 11
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
| 171 | 165, 170 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ 𝑋) |
| 172 | 171 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → 𝑦 ∈ 𝑋) |
| 173 | 86 | ntrss2 23065 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ (𝐴‘𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛)) |
| 174 | 85, 160, 173 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛)) |
| 175 | | sstr2 3990 |
. . . . . . . . . . . . 13
⊢ ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (((int‘𝐽)‘(𝐴‘𝑛)) ⊆ (𝐴‘𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
| 176 | 174, 175 | syl5com 31 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
| 177 | 176 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛))) |
| 178 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → 𝑦 ∈ 𝑋) |
| 179 | 178, 27 | jctil 519 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋)) |
| 180 | | rphalfcl 13062 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ+) |
| 181 | 180 | rpxrd 13078 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) ∈
ℝ*) |
| 182 | | rpxr 13044 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ*) |
| 183 | | rphalflt 13064 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (𝑥 / 2) < 𝑥) |
| 184 | 181, 182,
183 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ+
→ ((𝑥 / 2) ∈
ℝ* ∧ 𝑥
∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) |
| 185 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} |
| 186 | 14, 185 | blsscls2 24517 |
. . . . . . . . . . . . 13
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦 ∈ 𝑋) ∧ ((𝑥 / 2) ∈ ℝ* ∧ 𝑥 ∈ ℝ*
∧ (𝑥 / 2) < 𝑥)) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥)) |
| 187 | 179, 184,
186 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥)) |
| 188 | | sstr2 3990 |
. . . . . . . . . . . 12
⊢ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
| 189 | 187, 188 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴‘𝑛) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
| 190 | 180 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈
ℝ+) |
| 191 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2))) |
| 192 | 191 | rabbidv 3444 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 = (𝑥 / 2) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}) |
| 193 | 192 | sseq1d 4015 |
. . . . . . . . . . . . . 14
⊢ (𝑟 = (𝑥 / 2) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛))) |
| 194 | 193 | rspcev 3622 |
. . . . . . . . . . . . 13
⊢ (((𝑥 / 2) ∈ ℝ+
∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |
| 195 | 194 | ex 412 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 2) ∈ ℝ+
→ ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 196 | 190, 195 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴‘𝑛) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 197 | 177, 189,
196 | 3syld 60 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 198 | 197 | rexlimdva 3155 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ 𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 199 | 172, 198 | syldan 591 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 200 | 168, 199 | mpd 15 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |
| 201 | 200 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 202 | 163, 201 | jcad 512 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → (𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))) |
| 203 | 202 | eximdv 1917 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛)) → ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)))) |
| 204 | | n0 4353 |
. . . 4
⊢
(((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴‘𝑛))) |
| 205 | | df-rex 3071 |
. . . 4
⊢
(∃𝑦 ∈
𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛) ↔ ∃𝑦(𝑦 ∈ 𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 206 | 203, 204,
205 | 3imtr4g 296 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 207 | 206 | reximdva 3168 |
. 2
⊢ (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴‘𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛))) |
| 208 | 156, 207 | mpd 15 |
1
⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) |