Detailed syntax breakdown of Definition df-mopn
Step | Hyp | Ref
| Expression |
1 | | cmopn 12779 |
. 2
class
MetOpen |
2 | | vd |
. . 3
setvar 𝑑 |
3 | | cxmet 12774 |
. . . . 5
class
∞Met |
4 | 3 | crn 4612 |
. . . 4
class ran
∞Met |
5 | 4 | cuni 3796 |
. . 3
class ∪ ran ∞Met |
6 | 2 | cv 1347 |
. . . . . 6
class 𝑑 |
7 | | cbl 12776 |
. . . . . 6
class
ball |
8 | 6, 7 | cfv 5198 |
. . . . 5
class
(ball‘𝑑) |
9 | 8 | crn 4612 |
. . . 4
class ran
(ball‘𝑑) |
10 | | ctg 12594 |
. . . 4
class
topGen |
11 | 9, 10 | cfv 5198 |
. . 3
class
(topGen‘ran (ball‘𝑑)) |
12 | 2, 5, 11 | cmpt 4050 |
. 2
class (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran
(ball‘𝑑))) |
13 | 1, 12 | wceq 1348 |
1
wff MetOpen =
(𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran
(ball‘𝑑))) |