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

Definition df-mri 16013
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 = (𝑐 ran Moore ↦ {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
Distinct variable group:   𝑠,𝑐,𝑥

Detailed syntax breakdown of Definition df-mri
StepHypRef Expression
1 cmri 16009 . 2 class mrInd
2 vc . . 3 setvar 𝑐
3 cmre 16007 . . . . 5 class Moore
43crn 5025 . . . 4 class ran Moore
54cuni 4362 . . 3 class ran Moore
6 vx . . . . . . . 8 setvar 𝑥
76cv 1473 . . . . . . 7 class 𝑥
8 vs . . . . . . . . . 10 setvar 𝑠
98cv 1473 . . . . . . . . 9 class 𝑠
107csn 4120 . . . . . . . . 9 class {𝑥}
119, 10cdif 3532 . . . . . . . 8 class (𝑠 ∖ {𝑥})
122cv 1473 . . . . . . . . 9 class 𝑐
13 cmrc 16008 . . . . . . . . 9 class mrCls
1412, 13cfv 5786 . . . . . . . 8 class (mrCls‘𝑐)
1511, 14cfv 5786 . . . . . . 7 class ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
167, 15wcel 1975 . . . . . 6 wff 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1716wn 3 . . . . 5 wff ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1817, 6, 9wral 2891 . . . 4 wff 𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1912cuni 4362 . . . . 5 class 𝑐
2019cpw 4103 . . . 4 class 𝒫 𝑐
2118, 8, 20crab 2895 . . 3 class {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}
222, 5, 21cmpt 4633 . 2 class (𝑐 ran Moore ↦ {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
231, 22wceq 1474 1 wff mrInd = (𝑐 ran Moore ↦ {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
Colors of variables: wff setvar class
This definition is referenced by:  mrisval  16055
  Copyright terms: Public domain W3C validator