Metamath Proof Explorer


Theorem caufval

Description: The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Assertion caufval ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( Cau β€˜ 𝐷 ) = { 𝑓 ∈ ( 𝑋 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) } )

Proof

Step Hyp Ref Expression
1 df-cau ⊒ Cau = ( 𝑑 ∈ βˆͺ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) } )
2 dmeq ⊒ ( 𝑑 = 𝐷 β†’ dom 𝑑 = dom 𝐷 )
3 2 dmeqd ⊒ ( 𝑑 = 𝐷 β†’ dom dom 𝑑 = dom dom 𝐷 )
4 xmetf ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 : ( 𝑋 Γ— 𝑋 ) ⟢ ℝ* )
5 4 fdmd ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ dom 𝐷 = ( 𝑋 Γ— 𝑋 ) )
6 5 dmeqd ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ dom dom 𝐷 = dom ( 𝑋 Γ— 𝑋 ) )
7 dmxpid ⊒ dom ( 𝑋 Γ— 𝑋 ) = 𝑋
8 6 7 eqtrdi ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ dom dom 𝐷 = 𝑋 )
9 3 8 sylan9eqr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ dom dom 𝑑 = 𝑋 )
10 9 oveq1d ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( dom dom 𝑑 ↑pm β„‚ ) = ( 𝑋 ↑pm β„‚ ) )
11 simpr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ 𝑑 = 𝐷 )
12 11 fveq2d ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( ball β€˜ 𝑑 ) = ( ball β€˜ 𝐷 ) )
13 12 oveqd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) = ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) )
14 13 feq3d ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) ↔ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) ) )
15 14 rexbidv ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) ↔ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) ) )
16 15 ralbidv ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ ( βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) ↔ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) ) )
17 10 16 rabeqbidv ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑑 = 𝐷 ) β†’ { 𝑓 ∈ ( dom dom 𝑑 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝑑 ) π‘₯ ) } = { 𝑓 ∈ ( 𝑋 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) } )
18 fvssunirn ⊒ ( ∞Met β€˜ 𝑋 ) βŠ† βˆͺ ran ∞Met
19 18 sseli ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ 𝐷 ∈ βˆͺ ran ∞Met )
20 ovex ⊒ ( 𝑋 ↑pm β„‚ ) ∈ V
21 20 rabex ⊒ { 𝑓 ∈ ( 𝑋 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) } ∈ V
22 21 a1i ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ { 𝑓 ∈ ( 𝑋 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) } ∈ V )
23 1 17 19 22 fvmptd2 ⊒ ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) β†’ ( Cau β€˜ 𝐷 ) = { 𝑓 ∈ ( 𝑋 ↑pm β„‚ ) ∣ βˆ€ π‘₯ ∈ ℝ+ βˆƒ π‘˜ ∈ β„€ ( 𝑓 β†Ύ ( β„€β‰₯ β€˜ π‘˜ ) ) : ( β„€β‰₯ β€˜ π‘˜ ) ⟢ ( ( 𝑓 β€˜ π‘˜ ) ( ball β€˜ 𝐷 ) π‘₯ ) } )