Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-mopn | Structured version Visualization version GIF version |
Description: Define a function whose value is the family of open sets of a metric space. See elmopn 23576 for its main property. (Contributed by NM, 1-Sep-2006.) |
Ref | Expression |
---|---|
df-mopn | ⊢ MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmopn 20568 | . 2 class MetOpen | |
2 | vd | . . 3 setvar 𝑑 | |
3 | cxmet 20563 | . . . . 5 class ∞Met | |
4 | 3 | crn 5589 | . . . 4 class ran ∞Met |
5 | 4 | cuni 4844 | . . 3 class ∪ ran ∞Met |
6 | 2 | cv 1540 | . . . . . 6 class 𝑑 |
7 | cbl 20565 | . . . . . 6 class ball | |
8 | 6, 7 | cfv 6430 | . . . . 5 class (ball‘𝑑) |
9 | 8 | crn 5589 | . . . 4 class ran (ball‘𝑑) |
10 | ctg 17129 | . . . 4 class topGen | |
11 | 9, 10 | cfv 6430 | . . 3 class (topGen‘ran (ball‘𝑑)) |
12 | 2, 5, 11 | cmpt 5161 | . 2 class (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) |
13 | 1, 12 | wceq 1541 | 1 wff MetOpen = (𝑑 ∈ ∪ ran ∞Met ↦ (topGen‘ran (ball‘𝑑))) |
Colors of variables: wff setvar class |
This definition is referenced by: mopnval 23572 isxms2 23582 setsmstopn 23614 tngtopn 23795 |
Copyright terms: Public domain | W3C validator |