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 β€˜ 𝑑 ) π‘₯ ) } )