This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐷 ) 𝑥 ) } )