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 = c ∈ ⋃ ran ⁡ Moore ⟼ s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmri class mrInd
1 vc setvar c
2 cmre class Moore
3 2 crn class ran ⁡ Moore
4 3 cuni class ⋃ ran ⁡ Moore
5 vs setvar s
6 1 cv setvar c
7 6 cuni class ⋃ c
8 7 cpw class 𝒫 ⋃ c
9 vx setvar x
10 5 cv setvar s
11 9 cv setvar x
12 cmrc class mrCls
13 6 12 cfv class mrCls ⁡ c
14 11 csn class x
15 10 14 cdif class s ∖ x
16 15 13 cfv class mrCls ⁡ c ⁡ s ∖ x
17 11 16 wcel wff x ∈ mrCls ⁡ c ⁡ s ∖ x
18 17 wn wff ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x
19 18 9 10 wral wff ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x
20 19 5 8 crab class s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x
21 1 4 20 cmpt class c ∈ ⋃ ran ⁡ Moore ⟼ s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x
22 0 21 wceq wff mrInd = c ∈ ⋃ ran ⁡ Moore ⟼ s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x