Theorem mriss

Description: An independent set of a Moore system is a subset of the base set. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypothesis	mriss.1	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
Assertion	mriss	⊢ ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ⊆ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		mriss.1	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
2		eqid	⊢ ( mrCls ‘ 𝐴 ) = ( mrCls ‘ 𝐴 )
3	2 1	ismri	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( ( mrCls ‘ 𝐴 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
4	3	simprbda	⊢ ( ( 𝐴 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐼 ) → 𝑆 ⊆ 𝑋 )