df-cplmet

Description: A function which completes the given metric space. (Contributed by Mario Carneiro, 2-Dec-2014)

		Ref	Expression
	Assertion	df-cplmet	$⊢ cplMetSp = (w \in V ⟼ ⦋ ((w ↑_{𝑠} ℕ) ↾_{𝑠} Cau (dist (w))) / r ⦌ ⦋ {Base}_{r} / v ⦌ ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccpms	$class cplMetSp$
1		vw	$setvar w$
2		cvv	$class V$
3	1	cv	$setvar w$
4		cpws	$class ↑_{𝑠}$
5		cn	$class ℕ$
6	3 5 4	co	$class (w ↑_{𝑠} ℕ)$
7		cress	$class ↾_{𝑠}$
8		ccau	$class Cau$
9		cds	$class dist$
10	3 9	cfv	$class dist (w)$
11	10 8	cfv	$class Cau (dist (w))$
12	6 11 7	co	$class ((w ↑_{𝑠} ℕ) ↾_{𝑠} Cau (dist (w)))$
13		vr	$setvar r$
14		cbs	$class Base$
15	13	cv	$setvar r$
16	15 14	cfv	$class {Base}_{r}$
17		vv	$setvar v$
18		vf	$setvar f$
19		vg	$setvar g$
20	18	cv	$setvar f$
21	19	cv	$setvar g$
22	20 21	cpr	$class \{f, g\}$
23	17	cv	$setvar v$
24	22 23	wss	$wff \{f, g\} \subseteq v$
25		vx	$setvar x$
26		crp	$class ℝ^{+}$
27		vj	$setvar j$
28		cz	$class ℤ$
29		cuz	$class ℤ_{\geq}$
30	27	cv	$setvar j$
31	30 29	cfv	$class ℤ_{\geq j}$
32	20 31	cres	$class ({f ↾}_{ℤ_{\geq j}})$
33	30 21	cfv	$class g (j)$
34		cbl	$class ball$
35	10 34	cfv	$class ball (dist (w))$
36	25	cv	$setvar x$
37	33 36 35	co	$class (g (j) ball (dist (w)) x)$
38	31 37 32	wf	$wff ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x$
39	38 27 28	wrex	$wff \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x$
40	39 25 26	wral	$wff \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x$
41	24 40	wa	$wff (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)$
42	41 18 19	copab	$class \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\}$
43		ve	$setvar e$
44		cqus	$class /_{𝑠}$
45	43	cv	$setvar e$
46	15 45 44	co	$class (r /_{𝑠} e)$
47		csts	$class sSet$
48		cnx	$class ndx$
49	48 9	cfv	$class dist (ndx)$
50		vy	$setvar y$
51		vz	$setvar z$
52		vp	$setvar p$
53		vq	$setvar q$
54	52	cv	$setvar p$
55	54 45	cec	$class [p] e$
56	36 55	wceq	$wff x = [p] e$
57	50	cv	$setvar y$
58	53	cv	$setvar q$
59	58 45	cec	$class [q] e$
60	57 59	wceq	$wff y = [q] e$
61	56 60	wa	$wff (x = [p] e \land y = [q] e)$
62	15 9	cfv	$class dist (r)$
63	62	cof	$class \circ_{f} dist (r)$
64	54 58 63	co	$class (p {dist (r)}_{f} q)$
65		cli	$class ⇝$
66	51	cv	$setvar z$
67	64 66 65	wbr	$wff (p {dist (r)}_{f} q) ⇝ z$
68	61 67	wa	$wff ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)$
69	68 53 23	wrex	$wff \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)$
70	69 52 23	wrex	$wff \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)$
71	70 25 50 51	coprab	$class \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}$
72	49 71	cop	$class ⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩$
73	72	csn	$class \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\}$
74	46 73 47	co	$class ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\})$
75	43 42 74	csb	$class ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\})$
76	17 16 75	csb	$class ⦋ {Base}_{r} / v ⦌ ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\})$
77	13 12 76	csb	$class ⦋ ((w ↑_{𝑠} ℕ) ↾_{𝑠} Cau (dist (w))) / r ⦌ ⦋ {Base}_{r} / v ⦌ ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\})$
78	1 2 77	cmpt	$class (w \in V ⟼ ⦋ ((w ↑_{𝑠} ℕ) ↾_{𝑠} Cau (dist (w))) / r ⦌ ⦋ {Base}_{r} / v ⦌ ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\}))$
79	0 78	wceq	$wff cplMetSp = (w \in V ⟼ ⦋ ((w ↑_{𝑠} ℕ) ↾_{𝑠} Cau (dist (w))) / r ⦌ ⦋ {Base}_{r} / v ⦌ ⦋ \{⟨f, g⟩ \| (\{f, g\} \subseteq v \land \forall x \in ℝ^{+} \exists j \in ℤ ({f ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ g (j) ball (dist (w)) x)\} / e ⦌ ((r /_{𝑠} e) sSet \{⟨dist (ndx), \{⟨⟨x, y⟩, z⟩ \| \exists p \in v \exists q \in v ((x = [p] e \land y = [q] e) \land (p {dist (r)}_{f} q) ⇝ z)\}⟩\}))$

Metamath Proof Explorer

Definition df-cplmet

Detailed syntax breakdown