Definition df-mri

Description: In a Moore system, a set isindependent 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)

	Ref	Expression
Assertion	df-mri	$$⊢\mathrm{mrInd}=\left(c\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmri	$$class\mathrm{mrInd}$$
1		vc	$$setvarc$$
2		cmre	$$class\mathrm{Moore}$$
3	2	crn	$$class\mathrm{ran}\mathrm{Moore}$$
4	3	cuni	$$class\bigcup \mathrm{ran}\mathrm{Moore}$$
5		vs	$$setvars$$
6	1	cv	$$setvarc$$
7	6	cuni	$$class\bigcup c$$
8	7	cpw	$$class𝒫\bigcup c$$
9		vx	$$setvarx$$
10	5	cv	$$setvars$$
11	9	cv	$$setvarx$$
12		cmrc	$$class\mathrm{mrCls}$$
13	6 12	cfv	$$class\mathrm{mrCls}\left(c\right)$$
14	11	csn	$$class\left\{x\right\}$$
15	10 14	cdif	$$class\left(s\setminus \left\{x\right\}\right)$$
16	15 13	cfv	$$class\mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)$$
17	11 16	wcel	$$wffx\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)$$
18	17	wn	$$wff\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)$$
19	18 9 10	wral	$$wff\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)$$
20	19 5 8	crab	$$class\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}$$
21	1 4 20	cmpt	$$class\left(c\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}\right)$$
22	0 21	wceq	$$wff\mathrm{mrInd}=\left(c\in \bigcup \mathrm{ran}\mathrm{Moore}⟼\left\{s\in 𝒫\bigcup c|\forall x\in s\neg x\in \mathrm{mrCls}\left(c\right)\left(s\setminus \left\{x\right\}\right)\right\}\right)$$