Detailed syntax breakdown of Definition df-cusp
Step | Hyp | Ref
| Expression |
1 | | ccusp 23194 |
. 2
class
CUnifSp |
2 | | vc |
. . . . . . 7
setvar 𝑐 |
3 | 2 | cv 1542 |
. . . . . 6
class 𝑐 |
4 | | vw |
. . . . . . . . 9
setvar 𝑤 |
5 | 4 | cv 1542 |
. . . . . . . 8
class 𝑤 |
6 | | cuss 23151 |
. . . . . . . 8
class
UnifSt |
7 | 5, 6 | cfv 6380 |
. . . . . . 7
class
(UnifSt‘𝑤) |
8 | | ccfilu 23183 |
. . . . . . 7
class
CauFilu |
9 | 7, 8 | cfv 6380 |
. . . . . 6
class
(CauFilu‘(UnifSt‘𝑤)) |
10 | 3, 9 | wcel 2110 |
. . . . 5
wff 𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) |
11 | | ctopn 16926 |
. . . . . . . 8
class
TopOpen |
12 | 5, 11 | cfv 6380 |
. . . . . . 7
class
(TopOpen‘𝑤) |
13 | | cflim 22831 |
. . . . . . 7
class
fLim |
14 | 12, 3, 13 | co 7213 |
. . . . . 6
class
((TopOpen‘𝑤)
fLim 𝑐) |
15 | | c0 4237 |
. . . . . 6
class
∅ |
16 | 14, 15 | wne 2940 |
. . . . 5
wff
((TopOpen‘𝑤)
fLim 𝑐) ≠
∅ |
17 | 10, 16 | wi 4 |
. . . 4
wff (𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) |
18 | | cbs 16760 |
. . . . . 6
class
Base |
19 | 5, 18 | cfv 6380 |
. . . . 5
class
(Base‘𝑤) |
20 | | cfil 22742 |
. . . . 5
class
Fil |
21 | 19, 20 | cfv 6380 |
. . . 4
class
(Fil‘(Base‘𝑤)) |
22 | 17, 2, 21 | wral 3061 |
. . 3
wff
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) |
23 | | cusp 23152 |
. . 3
class
UnifSp |
24 | 22, 4, 23 | crab 3065 |
. 2
class {𝑤 ∈ UnifSp ∣
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)} |
25 | 1, 24 | wceq 1543 |
1
wff CUnifSp =
{𝑤 ∈ UnifSp ∣
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)} |