Definition df-mri 16248

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

Distinct variable group:   s, c, x

Detailed syntax breakdown of Definition df-mri

Step	Hyp	Ref	Expression
1		cmri 16244	. 2 class mrInd
2		vc	. . 3 setvar c
3		cmre 16242	. . . . 5 class Moore
4	3	crn 5115	. . . 4 class ran Moore
5	4	cuni 4436	. . 3 class U. ran Moore
6		vx	. . . . . . . 8 setvar x
7	6	cv 1482	. . . . . . 7 class x
8		vs	. . . . . . . . . 10 setvar s
9	8	cv 1482	. . . . . . . . 9 class s
10	7	csn 4177	. . . . . . . . 9 class { x }
11	9, 10	cdif 3571	. . . . . . . 8 class ( s \ { x } )
12	2	cv 1482	. . . . . . . . 9 class c
13		cmrc 16243	. . . . . . . . 9 class mrCls
14	12, 13	cfv 5888	. . . . . . . 8 class (mrCls ` c )
15	11, 14	cfv 5888	. . . . . . 7 class ( (mrCls ` c ) ` ( s \ { x } ) )
16	7, 15	wcel 1990	. . . . . 6 wff x e. ( (mrCls ` c ) ` ( s \ { x } ) )
17	16	wn 3	. . . . 5 wff -. x e. ( (mrCls ` c ) ` ( s \ { x } ) )
18	17, 6, 9	wral 2912	. . . 4 wff A. x e. s -. x e. ( (mrCls ` c ) ` ( s \ { x } ) )
19	12	cuni 4436	. . . . 5 class U. c
20	19	cpw 4158	. . . 4 class ~P U. c
21	18, 8, 20	crab 2916	. . 3 class { s e. ~P U. c | A. x e. s -. x e. ( (mrCls ` c ) ` ( s \ { x } ) ) }
22	2, 5, 21	cmpt 4729	. 2 class ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( (mrCls ` c ) ` ( s \ { x } ) ) } )
23	1, 22	wceq 1483	1 wff mrInd = ( c e. U. ran Moore |-> { s e. ~P U. c | A. x e. s -. x e. ( (mrCls ` c ) ` ( s \ { x } ) ) } )

This definition is referenced by:  mrisval  16290