Definition df-cau 25214

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 25211	. 2 class Cau
2		vd	. . 3 setvar 𝑑
3		cxmet 21268	. . . . 5 class ∞Met
4	3	crn 5678	. . . 4 class ran ∞Met
5	4	cuni 4908	. . 3 class ∪ ran ∞Met
6		vj	. . . . . . . . 9 setvar 𝑗
7	6	cv 1532	. . . . . . . 8 class 𝑗
8		cuz 12852	. . . . . . . 8 class ℤ≥
9	7, 8	cfv 6547	. . . . . . 7 class (ℤ≥‘𝑗)
10		vf	. . . . . . . . . 10 setvar 𝑓
11	10	cv 1532	. . . . . . . . 9 class 𝑓
12	7, 11	cfv 6547	. . . . . . . 8 class (𝑓‘𝑗)
13		vx	. . . . . . . . 9 setvar 𝑥
14	13	cv 1532	. . . . . . . 8 class 𝑥
15	2	cv 1532	. . . . . . . . 9 class 𝑑
16		cbl 21270	. . . . . . . . 9 class ball
17	15, 16	cfv 6547	. . . . . . . 8 class (ball‘𝑑)
18	12, 14, 17	co 7417	. . . . . . 7 class ((𝑓‘𝑗)(ball‘𝑑)𝑥)
19	11, 9	cres 5679	. . . . . . 7 class (𝑓 ↾ (ℤ≥‘𝑗))
20	9, 18, 19	wf 6543	. . . . . 6 wff (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
21		cz 12588	. . . . . 6 class ℤ
22	20, 6, 21	wrex 3060	. . . . 5 wff ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
23		crp 13006	. . . . 5 class ℝ+
24	22, 13, 23	wral 3051	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)
25	15	cdm 5677	. . . . . 6 class dom 𝑑
26	25	cdm 5677	. . . . 5 class dom dom 𝑑
27		cc 11136	. . . . 5 class ℂ
28		cpm 8844	. . . . 5 class ↑pm
29	26, 27, 28	co 7417	. . . 4 class (dom dom 𝑑 ↑pm ℂ)
30	24, 10, 29	crab 3419	. . 3 class {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}
31	2, 5, 30	cmpt 5231	. 2 class (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})
32	1, 31	wceq 1533	1 wff Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})

This definition is referenced by:  caufval  25233