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

Definition df-mri 16071
 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 16067 . 2 class mrInd
2 vc . . 3 setvar 𝑐
3 cmre 16065 . . . . 5 class Moore
43crn 5039 . . . 4 class ran Moore
54cuni 4372 . . 3 class ran Moore
6 vx . . . . . . . 8 setvar 𝑥
76cv 1474 . . . . . . 7 class 𝑥
8 vs . . . . . . . . . 10 setvar 𝑠
98cv 1474 . . . . . . . . 9 class 𝑠
107csn 4125 . . . . . . . . 9 class {𝑥}
119, 10cdif 3537 . . . . . . . 8 class (𝑠 ∖ {𝑥})
122cv 1474 . . . . . . . . 9 class 𝑐
13 cmrc 16066 . . . . . . . . 9 class mrCls
1412, 13cfv 5804 . . . . . . . 8 class (mrCls‘𝑐)
1511, 14cfv 5804 . . . . . . 7 class ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
167, 15wcel 1977 . . . . . 6 wff 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1716wn 3 . . . . 5 wff ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1817, 6, 9wral 2896 . . . 4 wff 𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
1912cuni 4372 . . . . 5 class 𝑐
2019cpw 4108 . . . 4 class 𝒫 𝑐
2118, 8, 20crab 2900 . . 3 class {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}
222, 5, 21cmpt 4643 . 2 class (𝑐 ran Moore ↦ {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
231, 22wceq 1475 1 wff mrInd = (𝑐 ran Moore ↦ {𝑠 ∈ 𝒫 𝑐 ∣ ∀𝑥𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
 Colors of variables: wff setvar class This definition is referenced by:  mrisval  16113
 Copyright terms: Public domain W3C validator