Definition df-mri 17214

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

Step	Hyp	Ref	Expression
1		cmri 17210	. 2 class mrInd
2		vc	. . 3 setvar 𝑐
3		cmre 17208	. . . . 5 class Moore
4	3	crn 5581	. . . 4 class ran Moore
5	4	cuni 4836	. . 3 class ∪ ran Moore
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1538	. . . . . . 7 class 𝑥
8		vs	. . . . . . . . . 10 setvar 𝑠
9	8	cv 1538	. . . . . . . . 9 class 𝑠
10	7	csn 4558	. . . . . . . . 9 class {𝑥}
11	9, 10	cdif 3880	. . . . . . . 8 class (𝑠 ∖ {𝑥})
12	2	cv 1538	. . . . . . . . 9 class 𝑐
13		cmrc 17209	. . . . . . . . 9 class mrCls
14	12, 13	cfv 6418	. . . . . . . 8 class (mrCls‘𝑐)
15	11, 14	cfv 6418	. . . . . . 7 class ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
16	7, 15	wcel 2108	. . . . . 6 wff 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
17	16	wn 3	. . . . 5 wff ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
18	17, 6, 9	wral 3063	. . . 4 wff ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
19	12	cuni 4836	. . . . 5 class ∪ 𝑐
20	19	cpw 4530	. . . 4 class 𝒫 ∪ 𝑐
21	18, 8, 20	crab 3067	. . 3 class {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}
22	2, 5, 21	cmpt 5153	. 2 class (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
23	1, 22	wceq 1539	1 wff mrInd = (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})

This definition is referenced by:  mrisval  17256