Detailed syntax breakdown of Definition df-cusp
Step | Hyp | Ref
| Expression |
1 | | ccusp 22908 |
. 2
class
CUnifSp |
2 | | vc |
. . . . . . 7
setvar 𝑐 |
3 | 2 | cv 1536 |
. . . . . 6
class 𝑐 |
4 | | vw |
. . . . . . . . 9
setvar 𝑤 |
5 | 4 | cv 1536 |
. . . . . . . 8
class 𝑤 |
6 | | cuss 22864 |
. . . . . . . 8
class
UnifSt |
7 | 5, 6 | cfv 6357 |
. . . . . . 7
class
(UnifSt‘𝑤) |
8 | | ccfilu 22897 |
. . . . . . 7
class
CauFilu |
9 | 7, 8 | cfv 6357 |
. . . . . 6
class
(CauFilu‘(UnifSt‘𝑤)) |
10 | 3, 9 | wcel 2114 |
. . . . 5
wff 𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) |
11 | | ctopn 16697 |
. . . . . . . 8
class
TopOpen |
12 | 5, 11 | cfv 6357 |
. . . . . . 7
class
(TopOpen‘𝑤) |
13 | | cflim 22544 |
. . . . . . 7
class
fLim |
14 | 12, 3, 13 | co 7158 |
. . . . . 6
class
((TopOpen‘𝑤)
fLim 𝑐) |
15 | | c0 4293 |
. . . . . 6
class
∅ |
16 | 14, 15 | wne 3018 |
. . . . 5
wff
((TopOpen‘𝑤)
fLim 𝑐) ≠
∅ |
17 | 10, 16 | wi 4 |
. . . 4
wff (𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) |
18 | | cbs 16485 |
. . . . . 6
class
Base |
19 | 5, 18 | cfv 6357 |
. . . . 5
class
(Base‘𝑤) |
20 | | cfil 22455 |
. . . . 5
class
Fil |
21 | 19, 20 | cfv 6357 |
. . . 4
class
(Fil‘(Base‘𝑤)) |
22 | 17, 2, 21 | wral 3140 |
. . 3
wff
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅) |
23 | | cusp 22865 |
. . 3
class
UnifSp |
24 | 22, 4, 23 | crab 3144 |
. 2
class {𝑤 ∈ UnifSp ∣
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)} |
25 | 1, 24 | wceq 1537 |
1
wff CUnifSp =
{𝑤 ∈ UnifSp ∣
∀𝑐 ∈
(Fil‘(Base‘𝑤))(𝑐 ∈
(CauFilu‘(UnifSt‘𝑤)) → ((TopOpen‘𝑤) fLim 𝑐) ≠ ∅)} |