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

Metamath Proof Explorer

Definition df-cau

Description: Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006)

Ref Expression
Assertion df-cau Cau = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccau ⊢ Cau
1 vd ⊢ 𝑑
2 cxmet ⊢ ∞Met
3 2 crn ⊢ ran ∞Met
4 3 cuni ⊢ ∪ ran ∞Met
5 vf ⊢ 𝑓
6 1 cv ⊢ 𝑑
7 6 cdm ⊢ dom 𝑑
8 7 cdm ⊢ dom dom 𝑑
9 cpm ⊢ ↑pm
10 cc ⊢ ℂ
11 8 10 9 co ⊢ ( dom dom 𝑑 ↑pm ℂ )
12 vx ⊢ 𝑥
13 crp ⊢ ℝ+
14 vj ⊢ 𝑗
15 cz ⊢ ℤ
16 5 cv ⊢ 𝑓
17 cuz ⊢ ℤ≥
18 14 cv ⊢ 𝑗
19 18 17 cfv ⊢ ( ℤ≥ ‘ 𝑗 )
20 16 19 cres ⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) )
21 18 16 cfv ⊢ ( 𝑓 ‘ 𝑗 )
22 cbl ⊢ ball
23 6 22 cfv ⊢ ( ball ‘ 𝑑 )
24 12 cv ⊢ 𝑥
25 21 24 23 co ⊢ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
26 19 25 20 wf ⊢ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
27 26 14 15 wrex ⊢ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
28 27 12 13 wral ⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 )
29 28 5 11 crab ⊢ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) }
30 1 4 29 cmpt ⊢ ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )
31 0 30 wceq ⊢ Cau = ( 𝑑 ∈ ∪ ran ∞Met ↦ { 𝑓 ∈ ( dom dom 𝑑 ↑pm ℂ ) ∣ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℤ ( 𝑓 ↾ ( ℤ≥ ‘ 𝑗 ) ) : ( ℤ≥ ‘ 𝑗 ) ⟶ ( ( 𝑓 ‘ 𝑗 ) ( ball ‘ 𝑑 ) 𝑥 ) } )