Detailed syntax breakdown of Definition df-cplmet
Step | Hyp | Ref
| Expression |
1 | | ccpms 33303 |
. 2
class
cplMetSp |
2 | | vw |
. . 3
setvar 𝑤 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vr |
. . . 4
setvar 𝑟 |
5 | 2 | cv 1542 |
. . . . . 6
class 𝑤 |
6 | | cn 11830 |
. . . . . 6
class
ℕ |
7 | | cpws 16951 |
. . . . . 6
class
↑s |
8 | 5, 6, 7 | co 7213 |
. . . . 5
class (𝑤 ↑s
ℕ) |
9 | | cds 16811 |
. . . . . . 7
class
dist |
10 | 5, 9 | cfv 6380 |
. . . . . 6
class
(dist‘𝑤) |
11 | | ccau 24150 |
. . . . . 6
class
Cau |
12 | 10, 11 | cfv 6380 |
. . . . 5
class
(Cau‘(dist‘𝑤)) |
13 | | cress 16784 |
. . . . 5
class
↾s |
14 | 8, 12, 13 | co 7213 |
. . . 4
class ((𝑤 ↑s
ℕ) ↾s (Cau‘(dist‘𝑤))) |
15 | | vv |
. . . . 5
setvar 𝑣 |
16 | 4 | cv 1542 |
. . . . . 6
class 𝑟 |
17 | | cbs 16760 |
. . . . . 6
class
Base |
18 | 16, 17 | cfv 6380 |
. . . . 5
class
(Base‘𝑟) |
19 | | ve |
. . . . . 6
setvar 𝑒 |
20 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
21 | 20 | cv 1542 |
. . . . . . . . . 10
class 𝑓 |
22 | | vg |
. . . . . . . . . . 11
setvar 𝑔 |
23 | 22 | cv 1542 |
. . . . . . . . . 10
class 𝑔 |
24 | 21, 23 | cpr 4543 |
. . . . . . . . 9
class {𝑓, 𝑔} |
25 | 15 | cv 1542 |
. . . . . . . . 9
class 𝑣 |
26 | 24, 25 | wss 3866 |
. . . . . . . 8
wff {𝑓, 𝑔} ⊆ 𝑣 |
27 | | vj |
. . . . . . . . . . . . 13
setvar 𝑗 |
28 | 27 | cv 1542 |
. . . . . . . . . . . 12
class 𝑗 |
29 | | cuz 12438 |
. . . . . . . . . . . 12
class
ℤ≥ |
30 | 28, 29 | cfv 6380 |
. . . . . . . . . . 11
class
(ℤ≥‘𝑗) |
31 | 28, 23 | cfv 6380 |
. . . . . . . . . . . 12
class (𝑔‘𝑗) |
32 | | vx |
. . . . . . . . . . . . 13
setvar 𝑥 |
33 | 32 | cv 1542 |
. . . . . . . . . . . 12
class 𝑥 |
34 | | cbl 20350 |
. . . . . . . . . . . . 13
class
ball |
35 | 10, 34 | cfv 6380 |
. . . . . . . . . . . 12
class
(ball‘(dist‘𝑤)) |
36 | 31, 33, 35 | co 7213 |
. . . . . . . . . . 11
class ((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥) |
37 | 21, 30 | cres 5553 |
. . . . . . . . . . 11
class (𝑓 ↾
(ℤ≥‘𝑗)) |
38 | 30, 36, 37 | wf 6376 |
. . . . . . . . . 10
wff (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥) |
39 | | cz 12176 |
. . . . . . . . . 10
class
ℤ |
40 | 38, 27, 39 | wrex 3062 |
. . . . . . . . 9
wff
∃𝑗 ∈
ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥) |
41 | | crp 12586 |
. . . . . . . . 9
class
ℝ+ |
42 | 40, 32, 41 | wral 3061 |
. . . . . . . 8
wff
∀𝑥 ∈
ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥) |
43 | 26, 42 | wa 399 |
. . . . . . 7
wff ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥)) |
44 | 43, 20, 22 | copab 5115 |
. . . . . 6
class
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} |
45 | 19 | cv 1542 |
. . . . . . . 8
class 𝑒 |
46 | | cqus 17010 |
. . . . . . . 8
class
/s |
47 | 16, 45, 46 | co 7213 |
. . . . . . 7
class (𝑟 /s 𝑒) |
48 | | cnx 16744 |
. . . . . . . . . 10
class
ndx |
49 | 48, 9 | cfv 6380 |
. . . . . . . . 9
class
(dist‘ndx) |
50 | | vp |
. . . . . . . . . . . . . . . . 17
setvar 𝑝 |
51 | 50 | cv 1542 |
. . . . . . . . . . . . . . . 16
class 𝑝 |
52 | 51, 45 | cec 8389 |
. . . . . . . . . . . . . . 15
class [𝑝]𝑒 |
53 | 33, 52 | wceq 1543 |
. . . . . . . . . . . . . 14
wff 𝑥 = [𝑝]𝑒 |
54 | | vy |
. . . . . . . . . . . . . . . 16
setvar 𝑦 |
55 | 54 | cv 1542 |
. . . . . . . . . . . . . . 15
class 𝑦 |
56 | | vq |
. . . . . . . . . . . . . . . . 17
setvar 𝑞 |
57 | 56 | cv 1542 |
. . . . . . . . . . . . . . . 16
class 𝑞 |
58 | 57, 45 | cec 8389 |
. . . . . . . . . . . . . . 15
class [𝑞]𝑒 |
59 | 55, 58 | wceq 1543 |
. . . . . . . . . . . . . 14
wff 𝑦 = [𝑞]𝑒 |
60 | 53, 59 | wa 399 |
. . . . . . . . . . . . 13
wff (𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) |
61 | 16, 9 | cfv 6380 |
. . . . . . . . . . . . . . . 16
class
(dist‘𝑟) |
62 | 61 | cof 7467 |
. . . . . . . . . . . . . . 15
class
∘f (dist‘𝑟) |
63 | 51, 57, 62 | co 7213 |
. . . . . . . . . . . . . 14
class (𝑝 ∘f
(dist‘𝑟)𝑞) |
64 | | vz |
. . . . . . . . . . . . . . 15
setvar 𝑧 |
65 | 64 | cv 1542 |
. . . . . . . . . . . . . 14
class 𝑧 |
66 | | cli 15045 |
. . . . . . . . . . . . . 14
class
⇝ |
67 | 63, 65, 66 | wbr 5053 |
. . . . . . . . . . . . 13
wff (𝑝 ∘f
(dist‘𝑟)𝑞) ⇝ 𝑧 |
68 | 60, 67 | wa 399 |
. . . . . . . . . . . 12
wff ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧) |
69 | 68, 56, 25 | wrex 3062 |
. . . . . . . . . . 11
wff
∃𝑞 ∈
𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧) |
70 | 69, 50, 25 | wrex 3062 |
. . . . . . . . . 10
wff
∃𝑝 ∈
𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧) |
71 | 70, 32, 54, 64 | coprab 7214 |
. . . . . . . . 9
class
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)} |
72 | 49, 71 | cop 4547 |
. . . . . . . 8
class
〈(dist‘ndx), {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉 |
73 | 72 | csn 4541 |
. . . . . . 7
class
{〈(dist‘ndx), {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉} |
74 | | csts 16716 |
. . . . . . 7
class
sSet |
75 | 47, 73, 74 | co 7213 |
. . . . . 6
class ((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉}) |
76 | 19, 44, 75 | csb 3811 |
. . . . 5
class
⦋{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉}) |
77 | 15, 18, 76 | csb 3811 |
. . . 4
class
⦋(Base‘𝑟) / 𝑣⦌⦋{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉}) |
78 | 4, 14, 77 | csb 3811 |
. . 3
class
⦋((𝑤
↑s ℕ) ↾s
(Cau‘(dist‘𝑤)))
/ 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉}) |
79 | 2, 3, 78 | cmpt 5135 |
. 2
class (𝑤 ∈ V ↦
⦋((𝑤
↑s ℕ) ↾s
(Cau‘(dist‘𝑤)))
/ 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉})) |
80 | 1, 79 | wceq 1543 |
1
wff cplMetSp =
(𝑤 ∈ V ↦
⦋((𝑤
↑s ℕ) ↾s
(Cau‘(dist‘𝑤)))
/ 𝑟⦌⦋(Base‘𝑟) / 𝑣⦌⦋{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾
(ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑔‘𝑗)(ball‘(dist‘𝑤))𝑥))} / 𝑒⦌((𝑟 /s 𝑒) sSet {〈(dist‘ndx),
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝑣 ∃𝑞 ∈ 𝑣 ((𝑥 = [𝑝]𝑒 ∧ 𝑦 = [𝑞]𝑒) ∧ (𝑝 ∘f (dist‘𝑟)𝑞) ⇝ 𝑧)}〉})) |