Metamath Proof Explorer
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 ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) |