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

Theorem caufval 23870
 Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.)
Assertion
Ref Expression
caufval (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)})
Distinct variable groups:   𝑓,𝑘,𝑥,𝐷   𝑓,𝑋,𝑘,𝑥

Proof of Theorem caufval
Dummy variable 𝑑 is distinct from all other variables.
StepHypRef Expression
1 df-cau 23851 . 2 Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥)})
2 dmeq 5755 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
32dmeqd 5757 . . . . 5 (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷)
4 xmetf 22927 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
54fdmd 6506 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
65dmeqd 5757 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → dom dom 𝐷 = dom (𝑋 × 𝑋))
7 dmxpid 5783 . . . . . 6 dom (𝑋 × 𝑋) = 𝑋
86, 7syl6eq 2875 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → dom dom 𝐷 = 𝑋)
93, 8sylan9eqr 2881 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋)
109oveq1d 7155 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (dom dom 𝑑pm ℂ) = (𝑋pm ℂ))
11 simpr 488 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
1211fveq2d 6657 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (ball‘𝑑) = (ball‘𝐷))
1312oveqd 7157 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑓𝑘)(ball‘𝑑)𝑥) = ((𝑓𝑘)(ball‘𝐷)𝑥))
1413feq3d 6484 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1514rexbidv 3289 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1615ralbidv 3191 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1710, 16rabeqbidv 3470 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥)} = {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)})
18 fvssunirn 6682 . . 3 (∞Met‘𝑋) ⊆ ran ∞Met
1918sseli 3947 . 2 (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ran ∞Met)
20 ovex 7173 . . . 4 (𝑋pm ℂ) ∈ V
2120rabex 5218 . . 3 {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)} ∈ V
2221a1i 11 . 2 (𝐷 ∈ (∞Met‘𝑋) → {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)} ∈ V)
231, 17, 19, 22fvmptd2 6759 1 (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2115  ∀wral 3132  ∃wrex 3133  {crab 3136  Vcvv 3479  ∪ cuni 4821   × cxp 5536  dom cdm 5538  ran crn 5539   ↾ cres 5540  ⟶wf 6334  ‘cfv 6338  (class class class)co 7140   ↑pm cpm 8392  ℂcc 10522  ℝ*cxr 10661  ℤcz 11969  ℤ≥cuz 12231  ℝ+crp 12377  ∞Metcxmet 20518  ballcbl 20520  Cauccau 23848 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5186  ax-nul 5193  ax-pow 5249  ax-pr 5313  ax-un 7446  ax-cnex 10580  ax-resscn 10581 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4822  df-br 5050  df-opab 5112  df-mpt 5130  df-id 5443  df-xp 5544  df-rel 5545  df-cnv 5546  df-co 5547  df-dm 5548  df-rn 5549  df-iota 6297  df-fun 6340  df-fn 6341  df-f 6342  df-fv 6346  df-ov 7143  df-oprab 7144  df-mpo 7145  df-map 8393  df-xr 10666  df-xmet 20526  df-cau 23851 This theorem is referenced by:  iscau  23871  equivcau  23895
 Copyright terms: Public domain W3C validator