Detailed syntax breakdown of Definition df-cmet
Step | Hyp | Ref
| Expression |
1 | | ccmet 24151 |
. 2
class
CMet |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | vd |
. . . . . . . . 9
setvar 𝑑 |
5 | 4 | cv 1542 |
. . . . . . . 8
class 𝑑 |
6 | | cmopn 20353 |
. . . . . . . 8
class
MetOpen |
7 | 5, 6 | cfv 6380 |
. . . . . . 7
class
(MetOpen‘𝑑) |
8 | | vf |
. . . . . . . 8
setvar 𝑓 |
9 | 8 | cv 1542 |
. . . . . . 7
class 𝑓 |
10 | | cflim 22831 |
. . . . . . 7
class
fLim |
11 | 7, 9, 10 | co 7213 |
. . . . . 6
class
((MetOpen‘𝑑)
fLim 𝑓) |
12 | | c0 4237 |
. . . . . 6
class
∅ |
13 | 11, 12 | wne 2940 |
. . . . 5
wff
((MetOpen‘𝑑)
fLim 𝑓) ≠
∅ |
14 | | ccfil 24149 |
. . . . . 6
class
CauFil |
15 | 5, 14 | cfv 6380 |
. . . . 5
class
(CauFil‘𝑑) |
16 | 13, 8, 15 | wral 3061 |
. . . 4
wff
∀𝑓 ∈
(CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅ |
17 | 2 | cv 1542 |
. . . . 5
class 𝑥 |
18 | | cmet 20349 |
. . . . 5
class
Met |
19 | 17, 18 | cfv 6380 |
. . . 4
class
(Met‘𝑥) |
20 | 16, 4, 19 | crab 3065 |
. . 3
class {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅} |
21 | 2, 3, 20 | cmpt 5135 |
. 2
class (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |
22 | 1, 21 | wceq 1543 |
1
wff CMet =
(𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) |