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

Definition df-mrc 13362
Description: Define the Moore closure of a generating set, which is the smallest closed set containing all generating elements. Definition of Moore closure in [Schechter] p. 79. This generalizes topological closure (mrccls 16648) and linear span (mrclsp 15581). (Contributed by Stefan O'Rear, 31-Jan-2015.)
Assertion
Ref Expression
df-mrc  |- mrCls  =  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^| { s  e.  c  |  x  C_  s } ) )
Distinct variable group:    s, c, x

Detailed syntax breakdown of Definition df-mrc
StepHypRef Expression
1 cmrc 13359 . 2  class mrCls
2 vc . . 3  set  c
3 cmre 13358 . . . . 5  class Moore
43crn 4581 . . . 4  class  ran Moore
54cuni 3727 . . 3  class  U. ran Moore
6 vx . . . 4  set  x
72cv 1618 . . . . . 6  class  c
87cuni 3727 . . . . 5  class  U. c
98cpw 3530 . . . 4  class  ~P U. c
106cv 1618 . . . . . . 7  class  x
11 vs . . . . . . . 8  set  s
1211cv 1618 . . . . . . 7  class  s
1310, 12wss 3078 . . . . . 6  wff  x  C_  s
1413, 11, 7crab 2512 . . . . 5  class  { s  e.  c  |  x 
C_  s }
1514cint 3760 . . . 4  class  |^| { s  e.  c  |  x 
C_  s }
166, 9, 15cmpt 3974 . . 3  class  ( x  e.  ~P U. c  |-> 
|^| { s  e.  c  |  x  C_  s } )
172, 5, 16cmpt 3974 . 2  class  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |-> 
|^| { s  e.  c  |  x  C_  s } ) )
181, 17wceq 1619 1  wff mrCls  =  ( c  e.  U. ran Moore  |->  ( x  e.  ~P U. c  |->  |^| { s  e.  c  |  x  C_  s } ) )
Colors of variables: wff set class
This definition is referenced by:  fnmrc  13381  mrcfval  13382
  Copyright terms: Public domain W3C validator