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

Theorem bcthlem2 23341
Description: Lemma for bcth 23345. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.)
Hypotheses
Ref Expression
bcth.2 𝐽 = (MetOpen‘𝐷)
bcthlem.4 (𝜑𝐷 ∈ (CMet‘𝑋))
bcthlem.5 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
bcthlem.6 (𝜑𝑀:ℕ⟶(Clsd‘𝐽))
bcthlem.7 (𝜑𝑅 ∈ ℝ+)
bcthlem.8 (𝜑𝐶𝑋)
bcthlem.9 (𝜑𝑔:ℕ⟶(𝑋 × ℝ+))
bcthlem.10 (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)
bcthlem.11 (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
Assertion
Ref Expression
bcthlem2 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
Distinct variable groups:   𝑘,𝑛,𝑟,𝑥,𝑧   𝐶,𝑟,𝑥   𝑔,𝑘,𝑛,𝑟,𝑥,𝑧,𝐷   𝑔,𝐹,𝑘,𝑛,𝑟,𝑥,𝑧   𝑔,𝐽,𝑘,𝑛,𝑟,𝑥,𝑧   𝑔,𝑀,𝑘,𝑛,𝑟,𝑥,𝑧   𝜑,𝑘,𝑛,𝑟,𝑥,𝑧   𝑥,𝑅   𝑔,𝑋,𝑘,𝑛,𝑟,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑔)   𝐶(𝑧,𝑔,𝑘,𝑛)   𝑅(𝑧,𝑔,𝑘,𝑛,𝑟)

Proof of Theorem bcthlem2
StepHypRef Expression
1 bcthlem.11 . . . . 5 (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)))
2 fvoveq1 6816 . . . . . . 7 (𝑘 = 𝑛 → (𝑔‘(𝑘 + 1)) = (𝑔‘(𝑛 + 1)))
3 id 22 . . . . . . . 8 (𝑘 = 𝑛𝑘 = 𝑛)
4 fveq2 6332 . . . . . . . 8 (𝑘 = 𝑛 → (𝑔𝑘) = (𝑔𝑛))
53, 4oveq12d 6811 . . . . . . 7 (𝑘 = 𝑛 → (𝑘𝐹(𝑔𝑘)) = (𝑛𝐹(𝑔𝑛)))
62, 5eleq12d 2844 . . . . . 6 (𝑘 = 𝑛 → ((𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ↔ (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛))))
76rspccva 3459 . . . . 5 ((∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔𝑘)) ∧ 𝑛 ∈ ℕ) → (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))
81, 7sylan 569 . . . 4 ((𝜑𝑛 ∈ ℕ) → (𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)))
9 bcthlem.9 . . . . . 6 (𝜑𝑔:ℕ⟶(𝑋 × ℝ+))
109ffvelrnda 6502 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (𝑔𝑛) ∈ (𝑋 × ℝ+))
11 bcth.2 . . . . . . 7 𝐽 = (MetOpen‘𝐷)
12 bcthlem.4 . . . . . . 7 (𝜑𝐷 ∈ (CMet‘𝑋))
13 bcthlem.5 . . . . . . 7 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝑋𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀𝑘))))})
1411, 12, 13bcthlem1 23340 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ℕ ∧ (𝑔𝑛) ∈ (𝑋 × ℝ+))) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)))))
1514expr 444 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ((𝑔𝑛) ∈ (𝑋 × ℝ+) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛))))))
1610, 15mpd 15 . . . 4 ((𝜑𝑛 ∈ ℕ) → ((𝑔‘(𝑛 + 1)) ∈ (𝑛𝐹(𝑔𝑛)) ↔ ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)))))
178, 16mpbid 222 . . 3 ((𝜑𝑛 ∈ ℕ) → ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛))))
18 cmetmet 23303 . . . . . . . . . . . . 13 (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
1912, 18syl 17 . . . . . . . . . . . 12 (𝜑𝐷 ∈ (Met‘𝑋))
20 metxmet 22359 . . . . . . . . . . . 12 (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
2119, 20syl 17 . . . . . . . . . . 11 (𝜑𝐷 ∈ (∞Met‘𝑋))
2211mopntop 22465 . . . . . . . . . . 11 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2321, 22syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ Top)
2423adantr 466 . . . . . . . . 9 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → 𝐽 ∈ Top)
25 xp1st 7347 . . . . . . . . . . . 12 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → (1st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋)
26 xp2nd 7348 . . . . . . . . . . . . 13 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ+)
2726rpxrd 12076 . . . . . . . . . . . 12 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → (2nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ*)
2825, 27jca 501 . . . . . . . . . . 11 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → ((1st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ*))
29 blssm 22443 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ*) → ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
30293expb 1113 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ ((1st ‘(𝑔‘(𝑛 + 1))) ∈ 𝑋 ∧ (2nd ‘(𝑔‘(𝑛 + 1))) ∈ ℝ*)) → ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
3121, 28, 30syl2an 583 . . . . . . . . . 10 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) ⊆ 𝑋)
32 1st2nd2 7354 . . . . . . . . . . . . 13 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → (𝑔‘(𝑛 + 1)) = ⟨(1st ‘(𝑔‘(𝑛 + 1))), (2nd ‘(𝑔‘(𝑛 + 1)))⟩)
3332fveq2d 6336 . . . . . . . . . . . 12 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑛 + 1))), (2nd ‘(𝑔‘(𝑛 + 1)))⟩))
34 df-ov 6796 . . . . . . . . . . . 12 ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘⟨(1st ‘(𝑔‘(𝑛 + 1))), (2nd ‘(𝑔‘(𝑛 + 1)))⟩)
3533, 34syl6reqr 2824 . . . . . . . . . . 11 ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))))
3635adantl 467 . . . . . . . . . 10 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → ((1st ‘(𝑔‘(𝑛 + 1)))(ball‘𝐷)(2nd ‘(𝑔‘(𝑛 + 1)))) = ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))))
3711mopnuni 22466 . . . . . . . . . . . 12 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
3821, 37syl 17 . . . . . . . . . . 11 (𝜑𝑋 = 𝐽)
3938adantr 466 . . . . . . . . . 10 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → 𝑋 = 𝐽)
4031, 36, 393sstr3d 3796 . . . . . . . . 9 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ 𝐽)
41 eqid 2771 . . . . . . . . . 10 𝐽 = 𝐽
4241sscls 21081 . . . . . . . . 9 ((𝐽 ∈ Top ∧ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ 𝐽) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))))
4324, 40, 42syl2anc 573 . . . . . . . 8 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))))
44 difss2 3890 . . . . . . . 8 (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)) → ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
45 sstr2 3759 . . . . . . . 8 (((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛))))
4643, 44, 45syl2im 40 . . . . . . 7 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛))))
4746a1d 25 . . . . . 6 ((𝜑 ∧ (𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+)) → ((2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))))
4847ex 397 . . . . 5 (𝜑 → ((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) → ((2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) → (((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛)) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛))))))
49483impd 1441 . . . 4 (𝜑 → (((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛))) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛))))
5049adantr 466 . . 3 ((𝜑𝑛 ∈ ℕ) → (((𝑔‘(𝑛 + 1)) ∈ (𝑋 × ℝ+) ∧ (2nd ‘(𝑔‘(𝑛 + 1))) < (1 / 𝑛) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘(𝑔‘(𝑛 + 1)))) ⊆ (((ball‘𝐷)‘(𝑔𝑛)) ∖ (𝑀𝑛))) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛))))
5117, 50mpd 15 . 2 ((𝜑𝑛 ∈ ℕ) → ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
5251ralrimiva 3115 1 (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔𝑛)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  cdif 3720  wss 3723  cop 4322   cuni 4574   class class class wbr 4786  {copab 4846   × cxp 5247  wf 6027  cfv 6031  (class class class)co 6793  cmpt2 6795  1st c1st 7313  2nd c2nd 7314  1c1 10139   + caddc 10141  *cxr 10275   < clt 10276   / cdiv 10886  cn 11222  +crp 12035  ∞Metcxmt 19946  Metcme 19947  ballcbl 19948  MetOpencmopn 19951  Topctop 20918  Clsdccld 21041  clsccl 21043  CMetcms 23271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-map 8011  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-n0 11495  df-z 11580  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-topgen 16312  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-top 20919  df-topon 20936  df-bases 20971  df-cld 21044  df-cls 21046  df-cmet 23274
This theorem is referenced by:  bcthlem3  23342  bcthlem4  23343
  Copyright terms: Public domain W3C validator