Definition df-cau 25577

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

Assertion

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

Distinct variable group:   𝑓,𝑑,𝑗,𝑥

Detailed syntax breakdown of Definition df-cau

Step	Hyp	Ref	Expression
1		ccau 25574	. 2 class Cau
2		vd	. . 3 setvar 𝑑
3		cxmet 21663	. . . . 5 class ∞Met
4	3	crn 5651	. . . 4 class ran ∞Met
5	4	cuni 4866	. . 3 class ∪ ran ∞Met
6		vj	. . . . . . . . 9 setvar 𝑗
7	6	cv 1568	. . . . . . . 8 class 𝑗
8		cuz 12965	. . . . . . . 8 class ℤ≥
9	7, 8	cfv 6538	. . . . . . 7 class (ℤ≥‘𝑗)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1568	. . . . . . . . 9 class 𝑓
12	7, 11	cfv 6538	. . . . . . . 8 class (𝑓‘𝑗)
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1568	. . . . . . . 8 class 𝑥
15	2	cv 1568	. . . . . . . . 9 class 𝑑
16		cbl 21665	. . . . . . . . 9 class ball
17	15, 16	cfv 6538	. . . . . . . 8 class (ball‘𝑑)
18	12, 14, 17	co 7420	. . . . . . 7 class ((𝑓‘𝑗)(ball‘𝑑)𝑥)
19	11, 9	cres 5652	. . . . . . 7 class (𝑓 ↾ (ℤ≥‘𝑗))
20	9, 18, 19	wf 6534	. . . . . 6 wff (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
21		cz 12693	. . . . . 6 class ℤ
22	20, 6, 21	wrex 3086	. . . . 5 wff ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
23		crp 13120	. . . . 5 class ℝ+
24	22, 13, 23	wral 3076	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
25	15	cdm 5650	. . . . . 6 class dom 𝑑
26	25	cdm 5650	. . . . 5 class dom dom 𝑑
27		cc 11198	. . . . 5 class ℂ
28		cpm 8848	. . . . 5 class ↑pm
29	26, 27, 28	co 7420	. . . 4 class (dom dom 𝑑 ↑pm ℂ)
30	24, 10, 29	crab 3412	. . 3 class {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}
31	2, 5, 30	cmpt 5185	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})
32	1, 31	wceq 1569	1 wff Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})

This definition is used by:  caufval  25596