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

Definition df-mri 13506
Description: In a Moore system, a set is independent if no element of the set is in the closure of the set with the element removed (Section 0.6 in [Gratzer] p. 27; Definition 4.1.1 in [FaureFrolicher] p. 83.) mrInd is a class function which takes a Moore system to its set of independent sets. (Contributed by David Moews, 1-May-2017.)
Assertion
Ref Expression
df-mri  |- mrInd  =  ( c  e.  U. ran Moore  |->  { s  e.  ~P U. c  |  A. x  e.  s  -.  x  e.  ( (mrCls `  c
) `  ( s  \  { x } ) ) } )
Distinct variable group:    s, c, x

Detailed syntax breakdown of Definition df-mri
StepHypRef Expression
1 cmri 13502 . 2  class mrInd
2 vc . . 3  set  c
3 cmre 13500 . . . . 5  class Moore
43crn 4706 . . . 4  class  ran Moore
54cuni 3843 . . 3  class  U. ran Moore
6 vx . . . . . . . 8  set  x
76cv 1631 . . . . . . 7  class  x
8 vs . . . . . . . . . 10  set  s
98cv 1631 . . . . . . . . 9  class  s
107csn 3653 . . . . . . . . 9  class  { x }
119, 10cdif 3162 . . . . . . . 8  class  ( s 
\  { x }
)
122cv 1631 . . . . . . . . 9  class  c
13 cmrc 13501 . . . . . . . . 9  class mrCls
1412, 13cfv 5271 . . . . . . . 8  class  (mrCls `  c )
1511, 14cfv 5271 . . . . . . 7  class  ( (mrCls `  c ) `  (
s  \  { x } ) )
167, 15wcel 1696 . . . . . 6  wff  x  e.  ( (mrCls `  c
) `  ( s  \  { x } ) )
1716wn 3 . . . . 5  wff  -.  x  e.  ( (mrCls `  c
) `  ( s  \  { x } ) )
1817, 6, 9wral 2556 . . . 4  wff  A. x  e.  s  -.  x  e.  ( (mrCls `  c
) `  ( s  \  { x } ) )
1912cuni 3843 . . . . 5  class  U. c
2019cpw 3638 . . . 4  class  ~P U. c
2118, 8, 20crab 2560 . . 3  class  { s  e.  ~P U. c  |  A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) }
222, 5, 21cmpt 4093 . 2  class  ( c  e.  U. ran Moore  |->  { s  e.  ~P U. c  |  A. x  e.  s  -.  x  e.  ( (mrCls `  c ) `  ( s  \  {
x } ) ) } )
231, 22wceq 1632 1  wff mrInd  =  ( c  e.  U. ran Moore  |->  { s  e.  ~P U. c  |  A. x  e.  s  -.  x  e.  ( (mrCls `  c
) `  ( s  \  { x } ) ) } )
Colors of variables: wff set class
This definition is referenced by:  mrisval  13548
  Copyright terms: Public domain W3C validator