Definition df-cplmet 34620

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), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))

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

Detailed syntax breakdown of Definition df-cplmet

Step	Hyp	Ref	Expression
1		ccpms 34613	. 2 class cplMetSp
2		vw	. . 3 setvar 𝑤
3		cvv 3474	. . 3 class V
4		vr	. . . 4 setvar 𝑟
5	2	cv 1540	. . . . . 6 class 𝑤
6		cn 12211	. . . . . 6 class ℕ
7		cpws 17391	. . . . . 6 class ↑s
8	5, 6, 7	co 7408	. . . . 5 class (𝑤 ↑s ℕ)
9		cds 17205	. . . . . . 7 class dist
10	5, 9	cfv 6543	. . . . . 6 class (dist‘𝑤)
11		ccau 24769	. . . . . 6 class Cau
12	10, 11	cfv 6543	. . . . 5 class (Cau‘(dist‘𝑤))
13		cress 17172	. . . . 5 class ↾s
14	8, 12, 13	co 7408	. . . 4 class ((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤)))
15		vv	. . . . 5 setvar 𝑣
16	4	cv 1540	. . . . . 6 class 𝑟
17		cbs 17143	. . . . . 6 class Base
18	16, 17	cfv 6543	. . . . 5 class (Base‘𝑟)
19		ve	. . . . . 6 setvar 𝑒
20		vf	. . . . . . . . . . 11 setvar 𝑓
21	20	cv 1540	. . . . . . . . . 10 class 𝑓
22		vg	. . . . . . . . . . 11 setvar 𝑔
23	22	cv 1540	. . . . . . . . . 10 class 𝑔
24	21, 23	cpr 4630	. . . . . . . . 9 class {𝑓, 𝑔}
25	15	cv 1540	. . . . . . . . 9 class 𝑣
26	24, 25	wss 3948	. . . . . . . 8 wff {𝑓, 𝑔} ⊆ 𝑣
27		vj	. . . . . . . . . . . . 13 setvar 𝑗
28	27	cv 1540	. . . . . . . . . . . 12 class 𝑗
29		cuz 12821	. . . . . . . . . . . 12 class ℤ≥
30	28, 29	cfv 6543	. . . . . . . . . . 11 class (ℤ≥‘𝑗)
31	28, 23	cfv 6543	. . . . . . . . . . . 12 class (𝑔‘𝑗)
32		vx	. . . . . . . . . . . . 13 setvar 𝑥
33	32	cv 1540	. . . . . . . . . . . 12 class 𝑥
34		cbl 20930	. . . . . . . . . . . . 13 class ball
35	10, 34	cfv 6543	. . . . . . . . . . . 12 class (ball‘(dist‘𝑤))
36	31, 33, 35	co 7408	. . . . . . . . . . 11 class ((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
37	21, 30	cres 5678	. . . . . . . . . . 11 class (𝑓 ↾ (ℤ≥‘𝑗))
38	30, 36, 37	wf 6539	. . . . . . . . . 10 wff (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
39		cz 12557	. . . . . . . . . 10 class ℤ
40	38, 27, 39	wrex 3070	. . . . . . . . 9 wff ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
41		crp 12973	. . . . . . . . 9 class ℝ+
42	40, 32, 41	wral 3061	. . . . . . . 8 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)
43	26, 42	wa 396	. . . . . . 7 wff ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))
44	43, 20, 22	copab 5210	. . . . . 6 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))}
45	19	cv 1540	. . . . . . . 8 class 𝑒
46		cqus 17450	. . . . . . . 8 class /s
47	16, 45, 46	co 7408	. . . . . . 7 class (𝑟 /s 𝑒)
48		cnx 17125	. . . . . . . . . 10 class ndx
49	48, 9	cfv 6543	. . . . . . . . 9 class (dist‘ndx)
50		vp	. . . . . . . . . . . . . . . . 17 setvar 𝑝
51	50	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑝
52	51, 45	cec 8700	. . . . . . . . . . . . . . 15 class [𝑝]𝑒
53	33, 52	wceq 1541	. . . . . . . . . . . . . 14 wff 𝑥 = [𝑝]𝑒
54		vy	. . . . . . . . . . . . . . . 16 setvar 𝑦
55	54	cv 1540	. . . . . . . . . . . . . . 15 class 𝑦
56		vq	. . . . . . . . . . . . . . . . 17 setvar 𝑞
57	56	cv 1540	. . . . . . . . . . . . . . . 16 class 𝑞
58	57, 45	cec 8700	. . . . . . . . . . . . . . 15 class [𝑞]𝑒
59	55, 58	wceq 1541	. . . . . . . . . . . . . 14 wff 𝑦 = [𝑞]𝑒
60	53, 59	wa 396	. . . . . . . . . . . . 13 wff (𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒)
61	16, 9	cfv 6543	. . . . . . . . . . . . . . . 16 class (dist‘𝑟)
62	61	cof 7667	. . . . . . . . . . . . . . 15 class ∘f (dist‘𝑟)
63	51, 57, 62	co 7408	. . . . . . . . . . . . . 14 class (𝑝 ∘f (dist‘𝑟)𝑞)
64		vz	. . . . . . . . . . . . . . 15 setvar 𝑧
65	64	cv 1540	. . . . . . . . . . . . . 14 class 𝑧
66		cli 15427	. . . . . . . . . . . . . 14 class ⇝
67	63, 65, 66	wbr 5148	. . . . . . . . . . . . 13 wff (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧
68	60, 67	wa 396	. . . . . . . . . . . 12 wff ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)
69	68, 56, 25	wrex 3070	. . . . . . . . . . 11 wff ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)
70	69, 50, 25	wrex 3070	. . . . . . . . . 10 wff ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)
71	70, 32, 54, 64	coprab 7409	. . . . . . . . 9 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}
72	49, 71	cop 4634	. . . . . . . 8 class ⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩
73	72	csn 4628	. . . . . . 7 class {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}
74		csts 17095	. . . . . . 7 class sSet
75	47, 73, 74	co 7408	. . . . . 6 class ((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
76	19, 44, 75	csb 3893	. . . . 5 class ⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
77	15, 18, 76	csb 3893	. . . 4 class ⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
78	4, 14, 77	csb 3893	. . 3 class ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
79	2, 3, 78	cmpt 5231	. 2 class (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
80	1, 79	wceq 1541	1 wff cplMetSp = (𝑤 ∈ V ↦ ⦋((𝑤 ↑s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))

This definition is referenced by: (None)