Definition df-mri 17556

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 17552	. 2 class mrInd
2		vc	. . 3 setvar 𝑐
3		cmre 17550	. . . . 5 class Moore
4	3	crn 5642	. . . 4 class ran Moore
5	4	cuni 4874	. . 3 class ∪ ran Moore
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1539	. . . . . . 7 class 𝑥
8		vs	. . . . . . . . . 10 setvar 𝑠
9	8	cv 1539	. . . . . . . . 9 class 𝑠
10	7	csn 4592	. . . . . . . . 9 class {𝑥}
11	9, 10	cdif 3914	. . . . . . . 8 class (𝑠 ∖ {𝑥})
12	2	cv 1539	. . . . . . . . 9 class 𝑐
13		cmrc 17551	. . . . . . . . 9 class mrCls
14	12, 13	cfv 6514	. . . . . . . 8 class (mrCls‘𝑐)
15	11, 14	cfv 6514	. . . . . . 7 class ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
16	7, 15	wcel 2109	. . . . . 6 wff 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
17	16	wn 3	. . . . 5 wff ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
18	17, 6, 9	wral 3045	. . . 4 wff ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))
19	12	cuni 4874	. . . . 5 class ∪ 𝑐
20	19	cpw 4566	. . . 4 class 𝒫 ∪ 𝑐
21	18, 8, 20	crab 3408	. . 3 class {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))}
22	2, 5, 21	cmpt 5191	. 2 class (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})
23	1, 22	wceq 1540	1 wff mrInd = (𝑐 ∈ ∪ ran Moore ↦ {𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ((mrCls‘𝑐)‘(𝑠 ∖ {𝑥}))})

This definition is referenced by:  mrisval  17598