Definition df-cplmet 31531

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

Assertion

Ref	Expression
df-cplmet	⊢ cplMetSp = (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))

Distinct variable group:   𝑒,𝑓,𝑔,𝑗,𝑝,𝑞,𝑟,𝑣,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-cplmet

Step	Hyp	Ref	Expression
1		ccpms 31523	. 2 class cplMetSp
2		vw	. . 3 setvar 𝑤
3		cvv 3200	. . 3 class V
4		vr	. . . 4 setvar 𝑟
5	2	cv 1482	. . . . . 6 class 𝑤
6		cn 11020	. . . . . 6 class ℕ
7		cpws 16107	. . . . . 6 class ↑s
8	5, 6, 7	co 6650	. . . . 5 class (𝑤 ↑s ℕ)
9		cds 15950	. . . . . . 7 class dist
10	5, 9	cfv 5888	. . . . . 6 class (dist‘𝑤)
11		cca 23051	. . . . . 6 class Cau
12	10, 11	cfv 5888	. . . . 5 class (Cau‘(dist‘𝑤))
13		cress 15858	. . . . 5 class ↾s
14	8, 12, 13	co 6650	. . . 4 class ((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤)))
15		vv	. . . . 5 setvar 𝑣
16	4	cv 1482	. . . . . 6 class 𝑟
17		cbs 15857	. . . . . 6 class Base
18	16, 17	cfv 5888	. . . . 5 class (Base‘𝑟)
19		ve	. . . . . 6 setvar 𝑒
20		vf	. . . . . . . . . . 11 setvar 𝑓
21	20	cv 1482	. . . . . . . . . 10 class 𝑓
22		vg	. . . . . . . . . . 11 setvar 𝑔
23	22	cv 1482	. . . . . . . . . 10 class 𝑔
24	21, 23	cpr 4179	. . . . . . . . 9 class {𝑓, 𝑔}
25	15	cv 1482	. . . . . . . . 9 class 𝑣
26	24, 25	wss 3574	. . . . . . . 8 wff {𝑓, 𝑔} ⊆ 𝑣
27		vj	. . . . . . . . . . . . 13 setvar 𝑗
28	27	cv 1482	. . . . . . . . . . . 12 class 𝑗
29		cuz 11687	. . . . . . . . . . . 12 class ℤ≥
30	28, 29	cfv 5888	. . . . . . . . . . 11 class (ℤ≥‘𝑗)
31	28, 23	cfv 5888	. . . . . . . . . . . 12 class (𝑔‘𝑗)
32		vx	. . . . . . . . . . . . 13 setvar 𝑥
33	32	cv 1482	. . . . . . . . . . . 12 class 𝑥
34		cbl 19733	. . . . . . . . . . . . 13 class ball
35	10, 34	cfv 5888	. . . . . . . . . . . 12 class (ball‘(dist‘𝑤))
36	31, 33, 35	co 6650	. . . . . . . . . . 11 class ((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
37	21, 30	cres 5116	. . . . . . . . . . 11 class (𝑓 ↾ (ℤ≥‘𝑗))
38	30, 36, 37	wf 5884	. . . . . . . . . 10 wff (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
39		cz 11377	. . . . . . . . . 10 class ℤ
40	38, 27, 39	wrex 2913	. . . . . . . . 9 wff ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
41		crp 11832	. . . . . . . . 9 class ℝ+
42	40, 32, 41	wral 2912	. . . . . . . 8 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
43	26, 42	wa 384	. . . . . . 7 wff ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))
44	43, 20, 22	copab 4712	. . . . . 6 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))}
45	19	cv 1482	. . . . . . . 8 class 𝑒
46		cqus 16165	. . . . . . . 8 class /s
47	16, 45, 46	co 6650	. . . . . . 7 class (𝑟 /s 𝑒)
48		cnx 15854	. . . . . . . . . 10 class ndx
49	48, 9	cfv 5888	. . . . . . . . 9 class (dist‘ndx)
50		vp	. . . . . . . . . . . . . . . . 17 setvar 𝑝
51	50	cv 1482	. . . . . . . . . . . . . . . 16 class 𝑝
52	51, 45	cec 7740	. . . . . . . . . . . . . . 15 class [𝑝]𝑒
53	33, 52	wceq 1483	. . . . . . . . . . . . . 14 wff 𝑥 = [𝑝]𝑒
54		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
55	54	cv 1482	. . . . . . . . . . . . . . 15 class 𝑦
56		vq	. . . . . . . . . . . . . . . . 17 setvar 𝑞
57	56	cv 1482	. . . . . . . . . . . . . . . 16 class 𝑞
58	57, 45	cec 7740	. . . . . . . . . . . . . . 15 class [𝑞]𝑒
59	55, 58	wceq 1483	. . . . . . . . . . . . . 14 wff 𝑦 = [𝑞]𝑒
60	53, 59	wa 384	. . . . . . . . . . . . 13 wff (𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒)
61	16, 9	cfv 5888	. . . . . . . . . . . . . . . 16 class (dist‘𝑟)
62	61	cof 6895	. . . . . . . . . . . . . . 15 class ∘𝑓 (dist‘𝑟)
63	51, 57, 62	co 6650	. . . . . . . . . . . . . 14 class (𝑝 ∘𝑓 (dist‘𝑟)𝑞)
64		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
65	64	cv 1482	. . . . . . . . . . . . . 14 class 𝑧
66		cli 14215	. . . . . . . . . . . . . 14 class ⇝
67	63, 65, 66	wbr 4653	. . . . . . . . . . . . 13 wff (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧
68	60, 67	wa 384	. . . . . . . . . . . 12 wff ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)
69	68, 56, 25	wrex 2913	. . . . . . . . . . 11 wff ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)
70	69, 50, 25	wrex 2913	. . . . . . . . . 10 wff ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)
71	70, 32, 54, 64	coprab 6651	. . . . . . . . 9 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}
72	49, 71	cop 4183	. . . . . . . 8 class ⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩
73	72	csn 4177	. . . . . . 7 class {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}
74		csts 15855	. . . . . . 7 class sSet
75	47, 73, 74	co 6650	. . . . . 6 class ((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
76	19, 44, 75	csb 3533	. . . . 5 class ⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
77	15, 18, 76	csb 3533	. . . 4 class ⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
78	4, 14, 77	csb 3533	. . 3 class ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
79	2, 3, 78	cmpt 4729	. 2 class (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
80	1, 79	wceq 1483	1 wff cplMetSp = (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘𝑓 (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))

This definition is referenced by: (None)