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	$$⊢\mathrm{Cau}=\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\left\{f\in \left(\mathrm{dom}\mathrm{dom}d{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccau	$$class\mathrm{Cau}$$
1		vd	$$setvard$$
2		cxmet	$$class\mathrm{\infty Met}$$
3	2	crn	$$class\mathrm{ran}\mathrm{\infty Met}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{\infty Met}$$
5		vf	$$setvarf$$
6	1	cv	$$setvard$$
7	6	cdm	$$class\mathrm{dom}d$$
8	7	cdm	$$class\mathrm{dom}\mathrm{dom}d$$
9		cpm	$$class{\uparrow }_{𝑝𝑚}$$
10		cc	$$classℂ$$
11	8 10 9	co	$$class\left(\mathrm{dom}\mathrm{dom}d{\uparrow }_{𝑝𝑚}ℂ\right)$$
12		vx	$$setvarx$$
13		crp	$$class{ℝ}^{+}$$
14		vj	$$setvarj$$
15		cz	$$class\mathbb{Z}$$
16	5	cv	$$setvarf$$
17		cuz	$$class{\mathbb{Z}}_{\ge }$$
18	14	cv	$$setvarj$$
19	18 17	cfv	$$class{\mathbb{Z}}_{\ge j}$$
20	16 19	cres	$$class\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)$$
21	18 16	cfv	$$classf\left(j\right)$$
22		cbl	$$class\mathrm{ball}$$
23	6 22	cfv	$$class\mathrm{ball}\left(d\right)$$
24	12	cv	$$setvarx$$
25	21 24 23	co	$$class\left(f\left(j\right)\mathrm{ball}\left(d\right)x\right)$$
26	19 25 20	wf	$$wff\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x$$
27	26 14 15	wrex	$$wff\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x$$
28	27 12 13	wral	$$wff\forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x$$
29	28 5 11	crab	$$class\left\{f\in \left(\mathrm{dom}\mathrm{dom}d{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x\right\}$$
30	1 4 29	cmpt	$$class\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\left\{f\in \left(\mathrm{dom}\mathrm{dom}d{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x\right\}\right)$$
31	0 30	wceq	$$wff\mathrm{Cau}=\left(d\in \bigcup \mathrm{ran}\mathrm{\infty Met}⟼\left\{f\in \left(\mathrm{dom}\mathrm{dom}d{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists j\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶f\left(j\right)\mathrm{ball}\left(d\right)x\right\}\right)$$