# Metamath Proof Explorer

## 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 ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )