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

Definition df-mri 13815
 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 Moore mrCls
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-mri
StepHypRef Expression
1 cmri 13811 . 2 mrInd
2 vc . . 3
3 cmre 13809 . . . . 5 Moore
43crn 4881 . . . 4 Moore
54cuni 4017 . . 3 Moore
6 vx . . . . . . . 8
76cv 1652 . . . . . . 7
8 vs . . . . . . . . . 10
98cv 1652 . . . . . . . . 9
107csn 3816 . . . . . . . . 9
119, 10cdif 3319 . . . . . . . 8
122cv 1652 . . . . . . . . 9
13 cmrc 13810 . . . . . . . . 9 mrCls
1412, 13cfv 5456 . . . . . . . 8 mrCls
1511, 14cfv 5456 . . . . . . 7 mrCls
167, 15wcel 1726 . . . . . 6 mrCls
1716wn 3 . . . . 5 mrCls
1817, 6, 9wral 2707 . . . 4 mrCls
1912cuni 4017 . . . . 5
2019cpw 3801 . . . 4
2118, 8, 20crab 2711 . . 3 mrCls
222, 5, 21cmpt 4268 . 2 Moore mrCls
231, 22wceq 1653 1 mrInd Moore mrCls
 Colors of variables: wff set class This definition is referenced by:  mrisval  13857
 Copyright terms: Public domain W3C validator