MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mopn Structured version   Visualization version   GIF version

Definition df-mopn 20602
Description: Define a function whose value is the family of open sets of a metric space. See elmopn 23604 for its main property. (Contributed by NM, 1-Sep-2006.)
Assertion
Ref Expression
df-mopn MetOpen = (𝑑 ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))

Detailed syntax breakdown of Definition df-mopn
StepHypRef Expression
1 cmopn 20596 . 2 class MetOpen
2 vd . . 3 setvar 𝑑
3 cxmet 20591 . . . . 5 class ∞Met
43crn 5591 . . . 4 class ran ∞Met
54cuni 4840 . . 3 class ran ∞Met
62cv 1538 . . . . . 6 class 𝑑
7 cbl 20593 . . . . . 6 class ball
86, 7cfv 6437 . . . . 5 class (ball‘𝑑)
98crn 5591 . . . 4 class ran (ball‘𝑑)
10 ctg 17157 . . . 4 class topGen
119, 10cfv 6437 . . 3 class (topGen‘ran (ball‘𝑑))
122, 5, 11cmpt 5158 . 2 class (𝑑 ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
131, 12wceq 1539 1 wff MetOpen = (𝑑 ran ∞Met ↦ (topGen‘ran (ball‘𝑑)))
Colors of variables: wff setvar class
This definition is referenced by:  mopnval  23600  isxms2  23610  setsmstopn  23642  tngtopn  23823
  Copyright terms: Public domain W3C validator