Definition df-cau 23577

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 23574	. 2 class Cau
2		vd	. . 3 setvar 𝑑
3		cxmet 20247	. . . . 5 class ∞Met
4	3	crn 5412	. . . 4 class ran ∞Met
5	4	cuni 4717	. . 3 class ∪ ran ∞Met
6		vj	. . . . . . . . 9 setvar 𝑗
7	6	cv 1507	. . . . . . . 8 class 𝑗
8		cuz 12064	. . . . . . . 8 class ℤ≥
9	7, 8	cfv 6193	. . . . . . 7 class (ℤ≥‘𝑗)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1507	. . . . . . . . 9 class 𝑓
12	7, 11	cfv 6193	. . . . . . . 8 class (𝑓‘𝑗)
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1507	. . . . . . . 8 class 𝑥
15	2	cv 1507	. . . . . . . . 9 class 𝑑
16		cbl 20249	. . . . . . . . 9 class ball
17	15, 16	cfv 6193	. . . . . . . 8 class (ball‘𝑑)
18	12, 14, 17	co 6982	. . . . . . 7 class ((𝑓‘𝑗)(ball‘𝑑)𝑥)
19	11, 9	cres 5413	. . . . . . 7 class (𝑓 ↾ (ℤ≥‘𝑗))
20	9, 18, 19	wf 6189	. . . . . 6 wff (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
21		cz 11799	. . . . . 6 class ℤ
22	20, 6, 21	wrex 3091	. . . . 5 wff ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
23		crp 12210	. . . . 5 class ℝ+
24	22, 13, 23	wral 3090	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
25	15	cdm 5411	. . . . . 6 class dom 𝑑
26	25	cdm 5411	. . . . 5 class dom dom 𝑑
27		cc 10339	. . . . 5 class ℂ
28		cpm 8213	. . . . 5 class ↑pm
29	26, 27, 28	co 6982	. . . 4 class (dom dom 𝑑 ↑pm ℂ)
30	24, 10, 29	crab 3094	. . 3 class {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}
31	2, 5, 30	cmpt 5013	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})
32	1, 31	wceq 1508	1 wff Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})

This definition is referenced by:  caufval  23596