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

Theorem caufval 24484
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 24465 . 2 Cau = (𝑑 ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥)})
2 dmeq 5825 . . . . . 6 (𝑑 = 𝐷 → dom 𝑑 = dom 𝐷)
32dmeqd 5827 . . . . 5 (𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷)
4 xmetf 23527 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
54fdmd 6641 . . . . . . 7 (𝐷 ∈ (∞Met‘𝑋) → dom 𝐷 = (𝑋 × 𝑋))
65dmeqd 5827 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → dom dom 𝐷 = dom (𝑋 × 𝑋))
7 dmxpid 5851 . . . . . 6 dom (𝑋 × 𝑋) = 𝑋
86, 7eqtrdi 2792 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → dom dom 𝐷 = 𝑋)
93, 8sylan9eqr 2798 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → dom dom 𝑑 = 𝑋)
109oveq1d 7322 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (dom dom 𝑑pm ℂ) = (𝑋pm ℂ))
11 simpr 486 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
1211fveq2d 6808 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (ball‘𝑑) = (ball‘𝐷))
1312oveqd 7324 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑓𝑘)(ball‘𝑑)𝑥) = ((𝑓𝑘)(ball‘𝐷)𝑥))
1413feq3d 6617 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → ((𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1514rexbidv 3172 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1615ralbidv 3171 . . 3 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → (∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥) ↔ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)))
1710, 16rabeqbidv 3427 . 2 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑑 = 𝐷) → {𝑓 ∈ (dom dom 𝑑pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝑑)𝑥)} = {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)})
18 fvssunirn 6835 . . 3 (∞Met‘𝑋) ⊆ ran ∞Met
1918sseli 3922 . 2 (𝐷 ∈ (∞Met‘𝑋) → 𝐷 ran ∞Met)
20 ovex 7340 . . . 4 (𝑋pm ℂ) ∈ V
2120rabex 5265 . . 3 {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)} ∈ V
2221a1i 11 . 2 (𝐷 ∈ (∞Met‘𝑋) → {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)} ∈ V)
231, 17, 19, 22fvmptd2 6915 1 (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋pm ℂ) ∣ ∀𝑥 ∈ ℝ+𝑘 ∈ ℤ (𝑓 ↾ (ℤ𝑘)):(ℤ𝑘)⟶((𝑓𝑘)(ball‘𝐷)𝑥)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1539  wcel 2104  wral 3062  wrex 3071  {crab 3284  Vcvv 3437   cuni 4844   × cxp 5598  dom cdm 5600  ran crn 5601  cres 5602  wf 6454  cfv 6458  (class class class)co 7307  pm cpm 8647  cc 10915  *cxr 11054  cz 12365  cuz 12628  +crp 12776  ∞Metcxmet 20627  ballcbl 20629  Cauccau 24462
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-resscn 10974
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-fv 6466  df-ov 7310  df-oprab 7311  df-mpo 7312  df-map 8648  df-xr 11059  df-xmet 20635  df-cau 24465
This theorem is referenced by:  iscau  24485  equivcau  24509
  Copyright terms: Public domain W3C validator