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

Definition df-mopn 16703
Description: Define a function whose value is the family of open sets of a metric space. See elmopn 18477 for its main property. (Contributed by NM, 1-Sep-2006.)
Assertion
Ref Expression
df-mopn  |-  MetOpen  =  ( d  e.  U. ran  * Met  |->  ( topGen `  ran  ( ball `  d )
) )

Detailed syntax breakdown of Definition df-mopn
StepHypRef Expression
1 cmopn 16696 . 2  class  MetOpen
2 vd . . 3  set  d
3 cxmt 16691 . . . . 5  class  * Met
43crn 4882 . . . 4  class  ran  * Met
54cuni 4017 . . 3  class  U. ran  * Met
62cv 1652 . . . . . 6  class  d
7 cbl 16693 . . . . . 6  class  ball
86, 7cfv 5457 . . . . 5  class  ( ball `  d )
98crn 4882 . . . 4  class  ran  ( ball `  d )
10 ctg 13670 . . . 4  class  topGen
119, 10cfv 5457 . . 3  class  ( topGen ` 
ran  ( ball `  d
) )
122, 5, 11cmpt 4269 . 2  class  ( d  e.  U. ran  * Met  |->  ( topGen `  ran  ( ball `  d )
) )
131, 12wceq 1653 1  wff  MetOpen  =  ( d  e.  U. ran  * Met  |->  ( topGen `  ran  ( ball `  d )
) )
Colors of variables: wff set class
This definition is referenced by:  mopnval  18473  isxms2  18483  setsmstopn  18513  tngtopn  18696
  Copyright terms: Public domain W3C validator