MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ubthlem1 Structured version   Visualization version   GIF version

Theorem ubthlem1 28951
Description: Lemma for ubth 28954. The function 𝐴 exhibits a countable collection of sets that are closed, being the inverse image under 𝑡 of the closed ball of radius 𝑘, and by assumption they cover 𝑋. Thus, by the Baire Category theorem bcth2 24227, for some 𝑛 the set 𝐴𝑛 has an interior, meaning that there is a closed ball {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
ubth.1 𝑋 = (BaseSet‘𝑈)
ubth.2 𝑁 = (normCV𝑊)
ubthlem.3 𝐷 = (IndMet‘𝑈)
ubthlem.4 𝐽 = (MetOpen‘𝐷)
ubthlem.5 𝑈 ∈ CBan
ubthlem.6 𝑊 ∈ NrmCVec
ubthlem.7 (𝜑𝑇 ⊆ (𝑈 BLnOp 𝑊))
ubthlem.8 (𝜑 → ∀𝑥𝑋𝑐 ∈ ℝ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐)
ubthlem.9 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
Assertion
Ref Expression
ubthlem1 (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦𝑋𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))
Distinct variable groups:   𝑘,𝑐,𝑛,𝑟,𝑥,𝑦,𝑧,𝐴   𝑡,𝑐,𝐷,𝑘,𝑛,𝑟,𝑥,𝑧   𝑘,𝐽,𝑛   𝑦,𝑡,𝐽,𝑥   𝑁,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝜑,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦   𝑇,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝑈,𝑐,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧   𝑊,𝑐,𝑛,𝑟,𝑡,𝑥,𝑦   𝑋,𝑐,𝑘,𝑛,𝑟,𝑡,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑡)   𝐷(𝑦)   𝑈(𝑘)   𝐽(𝑧,𝑟,𝑐)   𝑊(𝑧,𝑘)

Proof of Theorem ubthlem1
StepHypRef Expression
1 rzal 4420 . . . . . . . . 9 (𝑇 = ∅ → ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘)
21ralrimivw 3106 . . . . . . . 8 (𝑇 = ∅ → ∀𝑧𝑋𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘)
3 rabid2 3293 . . . . . . . 8 (𝑋 = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ↔ ∀𝑧𝑋𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘)
42, 3sylibr 237 . . . . . . 7 (𝑇 = ∅ → 𝑋 = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
54eqcomd 2743 . . . . . 6 (𝑇 = ∅ → {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} = 𝑋)
65eleq1d 2822 . . . . 5 (𝑇 = ∅ → ({𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽) ↔ 𝑋 ∈ (Clsd‘𝐽)))
7 iinrab 4977 . . . . . . 7 (𝑇 ≠ ∅ → 𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
87adantl 485 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → 𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
9 id 22 . . . . . . 7 (𝑇 ≠ ∅ → 𝑇 ≠ ∅)
10 ubthlem.7 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑇 ⊆ (𝑈 BLnOp 𝑊))
1110sselda 3901 . . . . . . . . . . . . . . . . . 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 28947 . . . . . . . . . . . . . . . . . . . . 21 (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec)
1917, 18ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 𝑈 ∈ NrmCVec
20 ubthlem.6 . . . . . . . . . . . . . . . . . . . 20 𝑊 ∈ NrmCVec
2112, 13, 14, 15, 16, 19, 20blocn2 28889 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))))
22 ubth.1 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑋 = (BaseSet‘𝑈)
2322, 12cbncms 28946 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋))
2417, 23ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22 𝐷 ∈ (CMet‘𝑋)
25 cmetmet 24183 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
26 metxmet 23232 . . . . . . . . . . . . . . . . . . . . . 22 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
2724, 25, 26mp2b 10 . . . . . . . . . . . . . . . . . . . . 21 𝐷 ∈ (∞Met‘𝑋)
2814mopntopon 23337 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋))
2927, 28ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 𝐽 ∈ (TopOn‘𝑋)
30 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (BaseSet‘𝑊) = (BaseSet‘𝑊)
3130, 13imsxmet 28773 . . . . . . . . . . . . . . . . . . . . . 22 (𝑊 ∈ NrmCVec → (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)))
3220, 31ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 (IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊))
3315mopntopon 23337 . . . . . . . . . . . . . . . . . . . . 21 ((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) → (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊)))
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))
35 iscncl 22166 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ (TopOn‘𝑋) ∧ (MetOpen‘(IndMet‘𝑊)) ∈ (TopOn‘(BaseSet‘𝑊))) → (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽))))
3629, 34, 35mp2an 692 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝐽 Cn (MetOpen‘(IndMet‘𝑊))) ↔ (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
3721, 36sylib 221 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝑈 BLnOp 𝑊) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
3811, 37syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝑇) → (𝑡:𝑋⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽)))
3938simpld 498 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
4039adantlr 715 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → 𝑡:𝑋⟶(BaseSet‘𝑊))
4140ffvelrnda 6904 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑥) ∈ (BaseSet‘𝑊))
4241biantrurd 536 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡𝑥)) ≤ 𝑘 ↔ ((𝑡𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡𝑥)) ≤ 𝑘)))
43 fveq2 6717 . . . . . . . . . . . . . . 15 (𝑦 = (𝑡𝑥) → (𝑁𝑦) = (𝑁‘(𝑡𝑥)))
4443breq1d 5063 . . . . . . . . . . . . . 14 (𝑦 = (𝑡𝑥) → ((𝑁𝑦) ≤ 𝑘 ↔ (𝑁‘(𝑡𝑥)) ≤ 𝑘))
4544elrab 3602 . . . . . . . . . . . . 13 ((𝑡𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} ↔ ((𝑡𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑁‘(𝑡𝑥)) ≤ 𝑘))
4642, 45bitr4di 292 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) ∧ 𝑥𝑋) → ((𝑁‘(𝑡𝑥)) ≤ 𝑘 ↔ (𝑡𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}))
4746pm5.32da 582 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → ((𝑥𝑋 ∧ (𝑁‘(𝑡𝑥)) ≤ 𝑘) ↔ (𝑥𝑋 ∧ (𝑡𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘})))
48 2fveq3 6722 . . . . . . . . . . . . . 14 (𝑧 = 𝑥 → (𝑁‘(𝑡𝑧)) = (𝑁‘(𝑡𝑥)))
4948breq1d 5063 . . . . . . . . . . . . 13 (𝑧 = 𝑥 → ((𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ (𝑁‘(𝑡𝑥)) ≤ 𝑘))
5049elrab 3602 . . . . . . . . . . . 12 (𝑥 ∈ {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ↔ (𝑥𝑋 ∧ (𝑁‘(𝑡𝑥)) ≤ 𝑘))
5150a1i 11 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ↔ (𝑥𝑋 ∧ (𝑁‘(𝑡𝑥)) ≤ 𝑘)))
52 ffn 6545 . . . . . . . . . . . 12 (𝑡:𝑋⟶(BaseSet‘𝑊) → 𝑡 Fn 𝑋)
53 elpreima 6878 . . . . . . . . . . . 12 (𝑡 Fn 𝑋 → (𝑥 ∈ (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}) ↔ (𝑥𝑋 ∧ (𝑡𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘})))
5440, 52, 533syl 18 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → (𝑥 ∈ (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}) ↔ (𝑥𝑋 ∧ (𝑡𝑥) ∈ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘})))
5547, 51, 543bitr4d 314 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → (𝑥 ∈ {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ↔ 𝑥 ∈ (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘})))
5655eqrdv 2735 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} = (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}))
57 imaeq2 5925 . . . . . . . . . . 11 (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} → (𝑡𝑥) = (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}))
5857eleq1d 2822 . . . . . . . . . 10 (𝑥 = {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} → ((𝑡𝑥) ∈ (Clsd‘𝐽) ↔ (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽)))
5938simprd 499 . . . . . . . . . . 11 ((𝜑𝑡𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽))
6059adantlr 715 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → ∀𝑥 ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊)))(𝑡𝑥) ∈ (Clsd‘𝐽))
61 nnre 11837 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
6261ad2antlr 727 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → 𝑘 ∈ ℝ)
6362rexrd 10883 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → 𝑘 ∈ ℝ*)
64 eqid 2737 . . . . . . . . . . . . . 14 (0vec𝑊) = (0vec𝑊)
6530, 64nvzcl 28715 . . . . . . . . . . . . 13 (𝑊 ∈ NrmCVec → (0vec𝑊) ∈ (BaseSet‘𝑊))
6620, 65ax-mp 5 . . . . . . . . . . . 12 (0vec𝑊) ∈ (BaseSet‘𝑊)
67 ubth.2 . . . . . . . . . . . . . . . . . 18 𝑁 = (normCV𝑊)
6830, 64, 67, 13nvnd 28769 . . . . . . . . . . . . . . . . 17 ((𝑊 ∈ NrmCVec ∧ 𝑦 ∈ (BaseSet‘𝑊)) → (𝑁𝑦) = (𝑦(IndMet‘𝑊)(0vec𝑊)))
6920, 68mpan 690 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (BaseSet‘𝑊) → (𝑁𝑦) = (𝑦(IndMet‘𝑊)(0vec𝑊)))
70 xmetsym 23245 . . . . . . . . . . . . . . . . 17 (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑦 ∈ (BaseSet‘𝑊)) → ((0vec𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec𝑊)))
7132, 66, 70mp3an12 1453 . . . . . . . . . . . . . . . 16 (𝑦 ∈ (BaseSet‘𝑊) → ((0vec𝑊)(IndMet‘𝑊)𝑦) = (𝑦(IndMet‘𝑊)(0vec𝑊)))
7269, 71eqtr4d 2780 . . . . . . . . . . . . . . 15 (𝑦 ∈ (BaseSet‘𝑊) → (𝑁𝑦) = ((0vec𝑊)(IndMet‘𝑊)𝑦))
7372breq1d 5063 . . . . . . . . . . . . . 14 (𝑦 ∈ (BaseSet‘𝑊) → ((𝑁𝑦) ≤ 𝑘 ↔ ((0vec𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘))
7473rabbiia 3382 . . . . . . . . . . . . 13 {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} = {𝑦 ∈ (BaseSet‘𝑊) ∣ ((0vec𝑊)(IndMet‘𝑊)𝑦) ≤ 𝑘}
7515, 74blcld 23403 . . . . . . . . . . . 12 (((IndMet‘𝑊) ∈ (∞Met‘(BaseSet‘𝑊)) ∧ (0vec𝑊) ∈ (BaseSet‘𝑊) ∧ 𝑘 ∈ ℝ*) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
7632, 66, 75mp3an12 1453 . . . . . . . . . . 11 (𝑘 ∈ ℝ* → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
7763, 76syl 17 . . . . . . . . . 10 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘} ∈ (Clsd‘(MetOpen‘(IndMet‘𝑊))))
7858, 60, 77rspcdva 3539 . . . . . . . . 9 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → (𝑡 “ {𝑦 ∈ (BaseSet‘𝑊) ∣ (𝑁𝑦) ≤ 𝑘}) ∈ (Clsd‘𝐽))
7956, 78eqeltrd 2838 . . . . . . . 8 (((𝜑𝑘 ∈ ℕ) ∧ 𝑡𝑇) → {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
8079ralrimiva 3105 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → ∀𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
81 iincld 21936 . . . . . . 7 ((𝑇 ≠ ∅ ∧ ∀𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽)) → 𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
829, 80, 81syl2anr 600 . . . . . 6 (((𝜑𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → 𝑡𝑇 {𝑧𝑋 ∣ (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
838, 82eqeltrrd 2839 . . . . 5 (((𝜑𝑘 ∈ ℕ) ∧ 𝑇 ≠ ∅) → {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
8414mopntop 23338 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
8527, 84ax-mp 5 . . . . . . 7 𝐽 ∈ Top
8629toponunii 21813 . . . . . . . 8 𝑋 = 𝐽
8786topcld 21932 . . . . . . 7 (𝐽 ∈ Top → 𝑋 ∈ (Clsd‘𝐽))
8885, 87ax-mp 5 . . . . . 6 𝑋 ∈ (Clsd‘𝐽)
8988a1i 11 . . . . 5 ((𝜑𝑘 ∈ ℕ) → 𝑋 ∈ (Clsd‘𝐽))
906, 83, 89pm2.61ne 3027 . . . 4 ((𝜑𝑘 ∈ ℕ) → {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ (Clsd‘𝐽))
91 ubthlem.9 . . . 4 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
9290, 91fmptd 6931 . . 3 (𝜑𝐴:ℕ⟶(Clsd‘𝐽))
9392frnd 6553 . . . . . 6 (𝜑 → ran 𝐴 ⊆ (Clsd‘𝐽))
9486cldss2 21927 . . . . . 6 (Clsd‘𝐽) ⊆ 𝒫 𝑋
9593, 94sstrdi 3913 . . . . 5 (𝜑 → ran 𝐴 ⊆ 𝒫 𝑋)
96 sspwuni 5008 . . . . 5 (ran 𝐴 ⊆ 𝒫 𝑋 ran 𝐴𝑋)
9795, 96sylib 221 . . . 4 (𝜑 ran 𝐴𝑋)
98 ubthlem.8 . . . . . 6 (𝜑 → ∀𝑥𝑋𝑐 ∈ ℝ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐)
99 arch 12087 . . . . . . . . . 10 (𝑐 ∈ ℝ → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
10099adantl 485 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) → ∃𝑘 ∈ ℕ 𝑐 < 𝑘)
101 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) → 𝑐 ∈ ℝ)
102 ltle 10921 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (𝑐 < 𝑘𝑐𝑘))
103101, 61, 102syl2an 599 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘𝑐𝑘))
104103impr 458 . . . . . . . . . . . . . . 15 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → 𝑐𝑘)
105104adantr 484 . . . . . . . . . . . . . 14 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → 𝑐𝑘)
10639ffvelrnda 6904 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑡𝑇) ∧ 𝑥𝑋) → (𝑡𝑥) ∈ (BaseSet‘𝑊))
107106an32s 652 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥𝑋) ∧ 𝑡𝑇) → (𝑡𝑥) ∈ (BaseSet‘𝑊))
10830, 67nvcl 28742 . . . . . . . . . . . . . . . . . 18 ((𝑊 ∈ NrmCVec ∧ (𝑡𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
10920, 107, 108sylancr 590 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥𝑋) ∧ 𝑡𝑇) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
110109adantlr 715 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑡𝑇) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
111110adantlr 715 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → (𝑁‘(𝑡𝑥)) ∈ ℝ)
112 simpllr 776 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → 𝑐 ∈ ℝ)
113 simplrl 777 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → 𝑘 ∈ ℕ)
114113, 61syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → 𝑘 ∈ ℝ)
115 letr 10926 . . . . . . . . . . . . . . 15 (((𝑁‘(𝑡𝑥)) ∈ ℝ ∧ 𝑐 ∈ ℝ ∧ 𝑘 ∈ ℝ) → (((𝑁‘(𝑡𝑥)) ≤ 𝑐𝑐𝑘) → (𝑁‘(𝑡𝑥)) ≤ 𝑘))
116111, 112, 114, 115syl3anc 1373 . . . . . . . . . . . . . 14 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → (((𝑁‘(𝑡𝑥)) ≤ 𝑐𝑐𝑘) → (𝑁‘(𝑡𝑥)) ≤ 𝑘))
117105, 116mpan2d 694 . . . . . . . . . . . . 13 (((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) ∧ 𝑡𝑇) → ((𝑁‘(𝑡𝑥)) ≤ 𝑐 → (𝑁‘(𝑡𝑥)) ≤ 𝑘))
118117ralimdva 3100 . . . . . . . . . . . 12 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ (𝑘 ∈ ℕ ∧ 𝑐 < 𝑘)) → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐 → ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘))
119118expr 460 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐 → ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘)))
12022fvexi 6731 . . . . . . . . . . . . . . . . . 18 𝑋 ∈ V
121120rabex 5225 . . . . . . . . . . . . . . . . 17 {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ V
12291fvmpt2 6829 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ ∧ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ∈ V) → (𝐴𝑘) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
123121, 122mpan2 691 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ → (𝐴𝑘) = {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘})
124123eleq2d 2823 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴𝑘) ↔ 𝑥 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘}))
12549ralbidv 3118 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑥 → (∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘 ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘))
126125elrab 3602 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝑧𝑋 ∣ ∀𝑡𝑇 (𝑁‘(𝑡𝑧)) ≤ 𝑘} ↔ (𝑥𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘))
127124, 126bitrdi 290 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → (𝑥 ∈ (𝐴𝑘) ↔ (𝑥𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘)))
128 simpr 488 . . . . . . . . . . . . . . . 16 ((𝜑𝑥𝑋) → 𝑥𝑋)
129128biantrurd 536 . . . . . . . . . . . . . . 15 ((𝜑𝑥𝑋) → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘 ↔ (𝑥𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘)))
130129bicomd 226 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → ((𝑥𝑋 ∧ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘) ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘))
131127, 130sylan9bbr 514 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴𝑘) ↔ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘))
13292ffnd 6546 . . . . . . . . . . . . . . 15 (𝜑𝐴 Fn ℕ)
133132adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑋) → 𝐴 Fn ℕ)
134 fnfvelrn 6901 . . . . . . . . . . . . . . . 16 ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴𝑘) ∈ ran 𝐴)
135 elssuni 4851 . . . . . . . . . . . . . . . 16 ((𝐴𝑘) ∈ ran 𝐴 → (𝐴𝑘) ⊆ ran 𝐴)
136134, 135syl 17 . . . . . . . . . . . . . . 15 ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝐴𝑘) ⊆ ran 𝐴)
137136sseld 3900 . . . . . . . . . . . . . 14 ((𝐴 Fn ℕ ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴𝑘) → 𝑥 ran 𝐴))
138133, 137sylan 583 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ ℕ) → (𝑥 ∈ (𝐴𝑘) → 𝑥 ran 𝐴))
139131, 138sylbird 263 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ ℕ) → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘𝑥 ran 𝐴))
140139adantlr 715 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑘𝑥 ran 𝐴))
141119, 140syl6d 75 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) ∧ 𝑘 ∈ ℕ) → (𝑐 < 𝑘 → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐𝑥 ran 𝐴)))
142141rexlimdva 3203 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) → (∃𝑘 ∈ ℕ 𝑐 < 𝑘 → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐𝑥 ran 𝐴)))
143100, 142mpd 15 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ℝ) → (∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐𝑥 ran 𝐴))
144143rexlimdva 3203 . . . . . . 7 ((𝜑𝑥𝑋) → (∃𝑐 ∈ ℝ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐𝑥 ran 𝐴))
145144ralimdva 3100 . . . . . 6 (𝜑 → (∀𝑥𝑋𝑐 ∈ ℝ ∀𝑡𝑇 (𝑁‘(𝑡𝑥)) ≤ 𝑐 → ∀𝑥𝑋 𝑥 ran 𝐴))
14698, 145mpd 15 . . . . 5 (𝜑 → ∀𝑥𝑋 𝑥 ran 𝐴)
147 dfss3 3888 . . . . 5 (𝑋 ran 𝐴 ↔ ∀𝑥𝑋 𝑥 ran 𝐴)
148146, 147sylibr 237 . . . 4 (𝜑𝑋 ran 𝐴)
14997, 148eqssd 3918 . . 3 (𝜑 ran 𝐴 = 𝑋)
150 eqid 2737 . . . . . 6 (0vec𝑈) = (0vec𝑈)
15122, 150nvzcl 28715 . . . . 5 (𝑈 ∈ NrmCVec → (0vec𝑈) ∈ 𝑋)
152 ne0i 4249 . . . . 5 ((0vec𝑈) ∈ 𝑋𝑋 ≠ ∅)
15319, 151, 152mp2b 10 . . . 4 𝑋 ≠ ∅
15414bcth2 24227 . . . 4 (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝐴:ℕ⟶(Clsd‘𝐽) ∧ ran 𝐴 = 𝑋)) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴𝑛)) ≠ ∅)
15524, 153, 154mpanl12 702 . . 3 ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ ran 𝐴 = 𝑋) → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴𝑛)) ≠ ∅)
15692, 149, 155syl2anc 587 . 2 (𝜑 → ∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴𝑛)) ≠ ∅)
157 ffvelrn 6902 . . . . . . . . . . 11 ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ (Clsd‘𝐽))
15894, 157sseldi 3899 . . . . . . . . . 10 ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ∈ 𝒫 𝑋)
159158elpwid 4524 . . . . . . . . 9 ((𝐴:ℕ⟶(Clsd‘𝐽) ∧ 𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑋)
16092, 159sylan 583 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ⊆ 𝑋)
16186ntrss3 21957 . . . . . . . 8 ((𝐽 ∈ Top ∧ (𝐴𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴𝑛)) ⊆ 𝑋)
16285, 160, 161sylancr 590 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴𝑛)) ⊆ 𝑋)
163162sseld 3900 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛)) → 𝑦𝑋))
16486ntropn 21946 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ (𝐴𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽)
16585, 160, 164sylancr 590 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽)
16614mopni2 23391 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)))
16727, 166mp3an1 1450 . . . . . . . . 9 ((((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)))
168165, 167sylan 583 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → ∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)))
169 elssuni 4851 . . . . . . . . . . . 12 (((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴𝑛)) ⊆ 𝐽)
170169, 86sseqtrrdi 3952 . . . . . . . . . . 11 (((int‘𝐽)‘(𝐴𝑛)) ∈ 𝐽 → ((int‘𝐽)‘(𝐴𝑛)) ⊆ 𝑋)
171165, 170syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴𝑛)) ⊆ 𝑋)
172171sselda 3901 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → 𝑦𝑋)
17386ntrss2 21954 . . . . . . . . . . . . . 14 ((𝐽 ∈ Top ∧ (𝐴𝑛) ⊆ 𝑋) → ((int‘𝐽)‘(𝐴𝑛)) ⊆ (𝐴𝑛))
17485, 160, 173sylancr 590 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → ((int‘𝐽)‘(𝐴𝑛)) ⊆ (𝐴𝑛))
175 sstr2 3908 . . . . . . . . . . . . 13 ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → (((int‘𝐽)‘(𝐴𝑛)) ⊆ (𝐴𝑛) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴𝑛)))
176174, 175syl5com 31 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴𝑛)))
177176ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → (𝑦(ball‘𝐷)𝑥) ⊆ (𝐴𝑛)))
178 simpr 488 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) → 𝑦𝑋)
179178, 27jctil 523 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) → (𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋))
180 rphalfcl 12613 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ+)
181180rpxrd 12629 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (𝑥 / 2) ∈ ℝ*)
182 rpxr 12595 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+𝑥 ∈ ℝ*)
183 rphalflt 12615 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ+ → (𝑥 / 2) < 𝑥)
184181, 182, 1833jca 1130 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+ → ((𝑥 / 2) ∈ ℝ*𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥))
185 eqid 2737 . . . . . . . . . . . . . 14 {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} = {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)}
18614, 185blsscls2 23402 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑦𝑋) ∧ ((𝑥 / 2) ∈ ℝ*𝑥 ∈ ℝ* ∧ (𝑥 / 2) < 𝑥)) → {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
187179, 184, 186syl2an 599 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥))
188 sstr2 3908 . . . . . . . . . . . 12 ({𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝑦(ball‘𝐷)𝑥) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴𝑛) → {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛)))
189187, 188syl 17 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ (𝐴𝑛) → {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛)))
190180adantl 485 . . . . . . . . . . . 12 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → (𝑥 / 2) ∈ ℝ+)
191 breq2 5057 . . . . . . . . . . . . . . . 16 (𝑟 = (𝑥 / 2) → ((𝑦𝐷𝑧) ≤ 𝑟 ↔ (𝑦𝐷𝑧) ≤ (𝑥 / 2)))
192191rabbidv 3390 . . . . . . . . . . . . . . 15 (𝑟 = (𝑥 / 2) → {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} = {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)})
193192sseq1d 3932 . . . . . . . . . . . . . 14 (𝑟 = (𝑥 / 2) → ({𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛) ↔ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛)))
194193rspcev 3537 . . . . . . . . . . . . 13 (((𝑥 / 2) ∈ ℝ+ ∧ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))
195194ex 416 . . . . . . . . . . . 12 ((𝑥 / 2) ∈ ℝ+ → ({𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
196190, 195syl 17 . . . . . . . . . . 11 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → ({𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ (𝑥 / 2)} ⊆ (𝐴𝑛) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
197177, 189, 1963syld 60 . . . . . . . . . 10 ((((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) ∧ 𝑥 ∈ ℝ+) → ((𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
198197rexlimdva 3203 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑋) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
199172, 198syldan 594 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → (∃𝑥 ∈ ℝ+ (𝑦(ball‘𝐷)𝑥) ⊆ ((int‘𝐽)‘(𝐴𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
200168, 199mpd 15 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛))) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))
201200ex 416 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛)) → ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
202163, 201jcad 516 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛)) → (𝑦𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))))
203202eximdv 1925 . . . 4 ((𝜑𝑛 ∈ ℕ) → (∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛)) → ∃𝑦(𝑦𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))))
204 n0 4261 . . . 4 (((int‘𝐽)‘(𝐴𝑛)) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ ((int‘𝐽)‘(𝐴𝑛)))
205 df-rex 3067 . . . 4 (∃𝑦𝑋𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛) ↔ ∃𝑦(𝑦𝑋 ∧ ∃𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
206203, 204, 2053imtr4g 299 . . 3 ((𝜑𝑛 ∈ ℕ) → (((int‘𝐽)‘(𝐴𝑛)) ≠ ∅ → ∃𝑦𝑋𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
207206reximdva 3193 . 2 (𝜑 → (∃𝑛 ∈ ℕ ((int‘𝐽)‘(𝐴𝑛)) ≠ ∅ → ∃𝑛 ∈ ℕ ∃𝑦𝑋𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛)))
208156, 207mpd 15 1 (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦𝑋𝑟 ∈ ℝ+ {𝑧𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴𝑛))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3408  wss 3866  c0 4237  𝒫 cpw 4513   cuni 4819   ciin 4905   class class class wbr 5053  cmpt 5135  ccnv 5550  ran crn 5552  cima 5554   Fn wfn 6375  wf 6376  cfv 6380  (class class class)co 7213  cr 10728  *cxr 10866   < clt 10867  cle 10868   / cdiv 11489  cn 11830  2c2 11885  +crp 12586  ∞Metcxmet 20348  Metcmet 20349  ballcbl 20350  MetOpencmopn 20353  Topctop 21790  TopOnctopon 21807  Clsdccld 21913  intcnt 21914   Cn ccn 22121  CMetccmet 24151  NrmCVeccnv 28665  BaseSetcba 28667  0veccn0v 28669  normCVcnmcv 28671  IndMetcims 28672   BLnOp cblo 28823  CBanccbn 28943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-dc 10060  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807  ax-addf 10808  ax-mulf 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-iin 4907  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-map 8510  df-pm 8511  df-en 8627  df-dom 8628  df-sdom 8629  df-sup 9058  df-inf 9059  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-n0 12091  df-z 12177  df-uz 12439  df-q 12545  df-rp 12587  df-xneg 12704  df-xadd 12705  df-xmul 12706  df-ico 12941  df-seq 13575  df-exp 13636  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-rest 16927  df-topgen 16948  df-psmet 20355  df-xmet 20356  df-met 20357  df-bl 20358  df-mopn 20359  df-fbas 20360  df-fg 20361  df-top 21791  df-topon 21808  df-bases 21843  df-cld 21916  df-ntr 21917  df-cls 21918  df-nei 21995  df-cn 22124  df-cnp 22125  df-lm 22126  df-fil 22743  df-fm 22835  df-flim 22836  df-flf 22837  df-cfil 24152  df-cau 24153  df-cmet 24154  df-grpo 28574  df-gid 28575  df-ginv 28576  df-gdiv 28577  df-ablo 28626  df-vc 28640  df-nv 28673  df-va 28676  df-ba 28677  df-sm 28678  df-0v 28679  df-vs 28680  df-nmcv 28681  df-ims 28682  df-lno 28825  df-nmoo 28826  df-blo 28827  df-0o 28828  df-cbn 28944
This theorem is referenced by:  ubthlem3  28953
  Copyright terms: Public domain W3C validator