Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cplmet Structured version   Visualization version   GIF version

Definition df-cplmet 33062
 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
StepHypRef Expression
1 ccpms 33054 . 2 class cplMetSp
2 vw . . 3 setvar 𝑤
3 cvv 3442 . . 3 class V
4 vr . . . 4 setvar 𝑟
52cv 1537 . . . . . 6 class 𝑤
6 cn 11643 . . . . . 6 class
7 cpws 16732 . . . . . 6 class s
85, 6, 7co 7145 . . . . 5 class (𝑤s ℕ)
9 cds 16586 . . . . . . 7 class dist
105, 9cfv 6332 . . . . . 6 class (dist‘𝑤)
11 ccau 23898 . . . . . 6 class Cau
1210, 11cfv 6332 . . . . 5 class (Cau‘(dist‘𝑤))
13 cress 16496 . . . . 5 class s
148, 12, 13co 7145 . . . 4 class ((𝑤s ℕ) ↾s (Cau‘(dist‘𝑤)))
15 vv . . . . 5 setvar 𝑣
164cv 1537 . . . . . 6 class 𝑟
17 cbs 16495 . . . . . 6 class Base
1816, 17cfv 6332 . . . . 5 class (Base‘𝑟)
19 ve . . . . . 6 setvar 𝑒
20 vf . . . . . . . . . . 11 setvar 𝑓
2120cv 1537 . . . . . . . . . 10 class 𝑓
22 vg . . . . . . . . . . 11 setvar 𝑔
2322cv 1537 . . . . . . . . . 10 class 𝑔
2421, 23cpr 4530 . . . . . . . . 9 class {𝑓, 𝑔}
2515cv 1537 . . . . . . . . 9 class 𝑣
2624, 25wss 3883 . . . . . . . 8 wff {𝑓, 𝑔} ⊆ 𝑣
27 vj . . . . . . . . . . . . 13 setvar 𝑗
2827cv 1537 . . . . . . . . . . . 12 class 𝑗
29 cuz 12251 . . . . . . . . . . . 12 class
3028, 29cfv 6332 . . . . . . . . . . 11 class (ℤ𝑗)
3128, 23cfv 6332 . . . . . . . . . . . 12 class (𝑔𝑗)
32 vx . . . . . . . . . . . . 13 setvar 𝑥
3332cv 1537 . . . . . . . . . . . 12 class 𝑥
34 cbl 20099 . . . . . . . . . . . . 13 class ball
3510, 34cfv 6332 . . . . . . . . . . . 12 class (ball‘(dist‘𝑤))
3631, 33, 35co 7145 . . . . . . . . . . 11 class ((𝑔𝑗)(ball‘(dist‘𝑤))𝑥)
3721, 30cres 5525 . . . . . . . . . . 11 class (𝑓 ↾ (ℤ𝑗))
3830, 36, 37wf 6328 . . . . . . . . . 10 wff (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥)
39 cz 11989 . . . . . . . . . 10 class
4038, 27, 39wrex 3107 . . . . . . . . 9 wff 𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥)
41 crp 12397 . . . . . . . . 9 class +
4240, 32, 41wral 3106 . . . . . . . 8 wff 𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥)
4326, 42wa 399 . . . . . . 7 wff ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))
4443, 20, 22copab 5096 . . . . . 6 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))}
4519cv 1537 . . . . . . . 8 class 𝑒
46 cqus 16790 . . . . . . . 8 class /s
4716, 45, 46co 7145 . . . . . . 7 class (𝑟 /s 𝑒)
48 cnx 16492 . . . . . . . . . 10 class ndx
4948, 9cfv 6332 . . . . . . . . 9 class (dist‘ndx)
50 vp . . . . . . . . . . . . . . . . 17 setvar 𝑝
5150cv 1537 . . . . . . . . . . . . . . . 16 class 𝑝
5251, 45cec 8288 . . . . . . . . . . . . . . 15 class [𝑝]𝑒
5333, 52wceq 1538 . . . . . . . . . . . . . 14 wff 𝑥 = [𝑝]𝑒
54 vy . . . . . . . . . . . . . . . 16 setvar 𝑦
5554cv 1537 . . . . . . . . . . . . . . 15 class 𝑦
56 vq . . . . . . . . . . . . . . . . 17 setvar 𝑞
5756cv 1537 . . . . . . . . . . . . . . . 16 class 𝑞
5857, 45cec 8288 . . . . . . . . . . . . . . 15 class [𝑞]𝑒
5955, 58wceq 1538 . . . . . . . . . . . . . 14 wff 𝑦 = [𝑞]𝑒
6053, 59wa 399 . . . . . . . . . . . . 13 wff (𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒)
6116, 9cfv 6332 . . . . . . . . . . . . . . . 16 class (dist‘𝑟)
6261cof 7398 . . . . . . . . . . . . . . 15 class f (dist‘𝑟)
6351, 57, 62co 7145 . . . . . . . . . . . . . 14 class (𝑝f (dist‘𝑟)𝑞)
64 vz . . . . . . . . . . . . . . 15 setvar 𝑧
6564cv 1537 . . . . . . . . . . . . . 14 class 𝑧
66 cli 14853 . . . . . . . . . . . . . 14 class
6763, 65, 66wbr 5034 . . . . . . . . . . . . 13 wff (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧
6860, 67wa 399 . . . . . . . . . . . 12 wff ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)
6968, 56, 25wrex 3107 . . . . . . . . . . 11 wff 𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)
7069, 50, 25wrex 3107 . . . . . . . . . 10 wff 𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)
7170, 32, 54, 64coprab 7146 . . . . . . . . 9 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}
7249, 71cop 4534 . . . . . . . 8 class ⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩
7372csn 4528 . . . . . . 7 class {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}
74 csts 16493 . . . . . . 7 class sSet
7547, 73, 74co 7145 . . . . . 6 class ((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
7619, 44, 75csb 3830 . . . . 5 class {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
7715, 18, 76csb 3830 . . . 4 class (Base‘𝑟) / 𝑣{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
784, 14, 77csb 3830 . . 3 class ((𝑤s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟(Base‘𝑟) / 𝑣{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩})
792, 3, 78cmpt 5114 . 2 class (𝑤 ∈ V ↦ ((𝑤s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟(Base‘𝑟) / 𝑣{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
801, 79wceq 1538 1 wff cplMetSp = (𝑤 ∈ V ↦ ((𝑤s ℕ) ↾s (Cau‘(dist‘𝑤))) / 𝑟(Base‘𝑟) / 𝑣{⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ (𝑓 ↾ (ℤ𝑗)):(ℤ𝑗)⟶((𝑔𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒((𝑟 /s 𝑒) sSet {⟨(dist‘ndx), {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ∃𝑝𝑣𝑞𝑣 ((𝑥 = [𝑝]𝑒𝑦 = [𝑞]𝑒) ∧ (𝑝f (dist‘𝑟)𝑞) ⇝ 𝑧)}⟩}))
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator