This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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