Metamath Proof Explorer


Theorem ismri2

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

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

Proof

Step Hyp Ref Expression
1 ismri2.1 𝑁 = ( mrCls ‘ 𝐴 )
2 ismri2.2 𝐼 = ( mrInd ‘ 𝐴 )
3 1 2 ismri ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆𝐼 ↔ ( 𝑆𝑋 ∧ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
4 3 baibd ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( 𝑆𝐼 ↔ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )