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	|- mrInd = ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmri	|- mrInd
1		vc	|- c
2		cmre	|- Moore
3	2	crn	|- ran Moore
4	3	cuni	|- U. ran Moore
5		vs	|- s
6	1	cv	|- c
7	6	cuni	|- U. c
8	7	cpw	|- ~P U. c
9		vx	|- x
10	5	cv	|- s
11	9	cv	|- x
12		cmrc	|- mrCls
13	6 12	cfv	|- ( mrCls ` c )
14	11	csn	|- { x }
15	10 14	cdif	|- ( s \ { x } )
16	15 13	cfv	|- ( ( mrCls ` c ) ` ( s \ { x } ) )
17	11 16	wcel	|- x e. ( ( mrCls ` c ) ` ( s \ { x } ) )
18	17	wn	|- -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) )
19	18 9 10	wral	|- A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) )
20	19 5 8	crab	|- { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) }
21	1 4 20	cmpt	|- ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } )
22	0 21	wceq	|- mrInd = ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( ( mrCls ` c ) ` ( s \ { x } ) ) } )