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 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
mrisval.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
Assertion mrisval ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐼 = { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )

Proof

Step Hyp Ref Expression
1 mrisval.1 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
2 mrisval.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
3 fvssunirn ⊢ ( Moore ‘ 𝑋 ) ⊆ ∪ ran Moore
4 3 sseli ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐴 ∈ ∪ ran Moore )
5 unieq ⊢ ( 𝑐 = 𝐴 → ∪ 𝑐 = ∪ 𝐴 )
6 5 pweqd ⊢ ( 𝑐 = 𝐴 → 𝒫 ∪ 𝑐 = 𝒫 ∪ 𝐴 )
7 fveq2 ⊢ ( 𝑐 = 𝐴 → ( mrCls ‘ 𝑐 ) = ( mrCls ‘ 𝐴 ) )
8 7 1 eqtr4di ⊢ ( 𝑐 = 𝐴 → ( mrCls ‘ 𝑐 ) = 𝑁 )
9 8 fveq1d ⊢ ( 𝑐 = 𝐴 → ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) )
10 9 eleq2d ⊢ ( 𝑐 = 𝐴 → ( 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ) )
11 10 notbid ⊢ ( 𝑐 = 𝐴 → ( ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ) )
12 11 ralbidv ⊢ ( 𝑐 = 𝐴 → ( ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ) )
13 6 12 rabeqbidv ⊢ ( 𝑐 = 𝐴 → { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } = { 𝑠 ∈ 𝒫 ∪ 𝐴 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
14 df-mri ⊢ mrInd = ( 𝑐 ∈ ∪ ran Moore ↦ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
15 vuniex ⊢ ∪ 𝑐 ∈ V
16 15 pwex ⊢ 𝒫 ∪ 𝑐 ∈ V
17 16 rabex ⊢ { 𝑠 ∈ 𝒫 ∪ 𝑐 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝑐 ) ‘ ( 𝑠 ∖ { 𝑥 } ) ) } ∈ V
18 13 14 17 fvmpt3i ⊢ ( 𝐴 ∈ ∪ ran Moore → ( mrInd ‘ 𝐴 ) = { 𝑠 ∈ 𝒫 ∪ 𝐴 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
19 4 18 syl ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( mrInd ‘ 𝐴 ) = { 𝑠 ∈ 𝒫 ∪ 𝐴 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
20 2 19 syl5eq ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐼 = { 𝑠 ∈ 𝒫 ∪ 𝐴 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
21 mreuni ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐴 = 𝑋 )
22 21 pweqd ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝒫 ∪ 𝐴 = 𝒫 𝑋 )
23 22 rabeqdv ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → { 𝑠 ∈ 𝒫 ∪ 𝐴 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } = { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
24 20 23 eqtrd ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐼 = { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )