Metamath Proof Explorer

Theorem mrisval

Description: Value of the set of independent sets of a Moore system. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses mrisval.1 ⊢ N = mrCls ⁡ A
mrisval.2 ⊢ I = mrInd ⁡ A
Assertion mrisval ⊢ A ∈ Moore ⁡ X → I = s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x

Proof

Step Hyp Ref Expression
1 mrisval.1 ⊢ N = mrCls ⁡ A
2 mrisval.2 ⊢ I = mrInd ⁡ A
3 fvssunirn ⊢ Moore ⁡ X ⊆ ⋃ ran ⁡ Moore
4 3 sseli ⊢ A ∈ Moore ⁡ X → A ∈ ⋃ ran ⁡ Moore
5 unieq ⊢ c = A → ⋃ c = ⋃ A
6 5 pweqd ⊢ c = A → 𝒫 ⋃ c = 𝒫 ⋃ A
7 fveq2 ⊢ c = A → mrCls ⁡ c = mrCls ⁡ A
8 7 1 eqtr4di ⊢ c = A → mrCls ⁡ c = N
9 8 fveq1d ⊢ c = A → mrCls ⁡ c ⁡ s ∖ x = N ⁡ s ∖ x
10 9 eleq2d ⊢ c = A → x ∈ mrCls ⁡ c ⁡ s ∖ x ↔ x ∈ N ⁡ s ∖ x
11 10 notbid ⊢ c = A → ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x ↔ ¬ x ∈ N ⁡ s ∖ x
12 11 ralbidv ⊢ c = A → ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x ↔ ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
13 6 12 rabeqbidv ⊢ c = A → s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x = s ∈ 𝒫 ⋃ A | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
14 df-mri ⊢ mrInd = c ∈ ⋃ ran ⁡ Moore ⟼ s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x
15 vuniex ⊢ ⋃ c ∈ V
16 15 pwex ⊢ 𝒫 ⋃ c ∈ V
17 16 rabex ⊢ s ∈ 𝒫 ⋃ c | ∀ x ∈ s ¬ x ∈ mrCls ⁡ c ⁡ s ∖ x ∈ V
18 13 14 17 fvmpt3i ⊢ A ∈ ⋃ ran ⁡ Moore → mrInd ⁡ A = s ∈ 𝒫 ⋃ A | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
19 4 18 syl ⊢ A ∈ Moore ⁡ X → mrInd ⁡ A = s ∈ 𝒫 ⋃ A | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
20 2 19 syl5eq ⊢ A ∈ Moore ⁡ X → I = s ∈ 𝒫 ⋃ A | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
21 mreuni ⊢ A ∈ Moore ⁡ X → ⋃ A = X
22 21 pweqd ⊢ A ∈ Moore ⁡ X → 𝒫 ⋃ A = 𝒫 X
23 22 rabeqdv ⊢ A ∈ Moore ⁡ X → s ∈ 𝒫 ⋃ A | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x = s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
24 20 23 eqtrd ⊢ A ∈ Moore ⁡ X → I = s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x