Metamath Proof Explorer

Definition 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 ∈ V ⟼ ⦋ w ↑ 𝑠 ℕ ↾ 𝑠 Cau ⁡ dist ⁡ w / r⦌ ⦋ Base r / v⦌ ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ 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 ⊆ v
25 vx setvar x
26 crp class ℝ +
27 vj setvar j
28 cz class ℤ
29 cuz class ℤ ≥
30 27 cv setvar j
31 30 29 cfv class ℤ ≥ j
32 20 31 cres class f ↾ ℤ ≥ 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 ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x
39 38 27 28 wrex wff ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x
40 39 25 26 wral wff ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x
41 24 40 wa wff f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x
42 41 18 19 copab class f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ 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 ∧ y = q e
62 15 9 cfv class dist ⁡ r
63 62 cof class ∘ 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 ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
69 68 53 23 wrex wff ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
70 69 52 23 wrex wff ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
71 70 25 50 51 coprab class x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
72 49 71 cop class dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
73 72 csn class dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
74 46 73 47 co class r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
75 43 42 74 csb class ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
76 17 16 75 csb class ⦋ Base r / v⦌ ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
77 13 12 76 csb class ⦋ w ↑ 𝑠 ℕ ↾ 𝑠 Cau ⁡ dist ⁡ w / r⦌ ⦋ Base r / v⦌ ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
78 1 2 77 cmpt class w ∈ V ⟼ ⦋ w ↑ 𝑠 ℕ ↾ 𝑠 Cau ⁡ dist ⁡ w / r⦌ ⦋ Base r / v⦌ ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z
79 0 78 wceq wff cplMetSp = w ∈ V ⟼ ⦋ w ↑ 𝑠 ℕ ↾ 𝑠 Cau ⁡ dist ⁡ w / r⦌ ⦋ Base r / v⦌ ⦋ f g | f g ⊆ v ∧ ∀ x ∈ ℝ + ∃ j ∈ ℤ f ↾ ℤ ≥ j : ℤ ≥ j ⟶ g ⁡ j ball ⁡ dist ⁡ w x / e⦌ r / 𝑠 e sSet dist ⁡ ndx x y z | ∃ p ∈ v ∃ q ∈ v x = p e ∧ y = q e ∧ p dist ⁡ r f q ⇝ z