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

Definition df-mri 15202
 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 15198 . 2 mrInd
2 vc . . 3
3 cmre 15196 . . . . 5 Moore
43crn 4824 . . . 4 Moore
54cuni 4191 . . 3 Moore
6 vx . . . . . . . 8
76cv 1404 . . . . . . 7
8 vs . . . . . . . . . 10
98cv 1404 . . . . . . . . 9
107csn 3972 . . . . . . . . 9
119, 10cdif 3411 . . . . . . . 8
122cv 1404 . . . . . . . . 9
13 cmrc 15197 . . . . . . . . 9 mrCls
1412, 13cfv 5569 . . . . . . . 8 mrCls
1511, 14cfv 5569 . . . . . . 7 mrCls
167, 15wcel 1842 . . . . . 6 mrCls
1716wn 3 . . . . 5 mrCls
1817, 6, 9wral 2754 . . . 4 mrCls
1912cuni 4191 . . . . 5
2019cpw 3955 . . . 4
2118, 8, 20crab 2758 . . 3 mrCls
222, 5, 21cmpt 4453 . 2 Moore mrCls
231, 22wceq 1405 1 mrInd Moore mrCls
 Colors of variables: wff setvar class This definition is referenced by:  mrisval  15244
 Copyright terms: Public domain W3C validator