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 = ( 𝑐 ∈ ∪ ran Moore ↦ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmri	⊢ mrInd
1		vc	⊢ 𝑐
2		cmre	⊢ Moore
3	2	crn	⊢ ran Moore
4	3	cuni	⊢ ∪ ran Moore
5		vs	⊢ 𝑠
6	1	cv	⊢ 𝑐
7	6	cuni	⊢ ∪ 𝑐
8	7	cpw	⊢ 𝒫 ∪ 𝑐
9		vx	⊢ 𝑥
10	5	cv	⊢ 𝑠
11	9	cv	⊢ 𝑥
12		cmrc	⊢ mrCls
13	6 12	cfv	⊢ ( mrCls ‘ 𝑐 )
14	11	csn	⊢ { 𝑥 }
15	10 14	cdif	⊢ ( 𝑠 ∖ { 𝑥 } )
16	15 13	cfv	⊢ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) )
17	11 16	wcel	⊢ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) )
18	17	wn	⊢ ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) )
19	18 9 10	wral	⊢ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) )
20	19 5 8	crab	⊢ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) }
21	1 4 20	cmpt	⊢ ( 𝑐 ∈ ∪ ran Moore ↦ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
22	0 21	wceq	⊢ mrInd = ( 𝑐 ∈ ∪ ran Moore ↦ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )