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

Metamath Proof Explorer

Theorem ismri

Description: Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses ismri.1 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
ismri.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
Assertion ismri ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismri.1 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
2 ismri.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
3 1 2 mrisval ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐼 = { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
4 3 eleq2d ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } ) )
5 difeq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑥 } ) )
6 5 fveq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
7 6 eleq2d ⊢ ( 𝑠 = 𝑆 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
8 7 notbid ⊢ ( 𝑠 = 𝑆 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
9 8 raleqbi1dv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
10 9 elrab ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
11 4 10 bitrdi ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
12 elfvex ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ V )
13 elpw2g ⊢ ( 𝑋 ∈ V → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
14 12 13 syl ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
15 14 anbi1d ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
16 11 15 bitrd ⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )