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

Metamath Proof Explorer

Theorem ismri2dd

Description: Definition of independence of a subset of the base set in a Moore system. One-way deduction form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri2.1	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	ismri2.2	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	ismri2d.3	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	ismri2d.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
	ismri2dd.5	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
Assertion	ismri2dd	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		ismri2.1	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
2		ismri2.2	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
3		ismri2d.3	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
4		ismri2d.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
5		ismri2dd.5	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
6	1 2 3 4	ismri2d	⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
7	5 6	mpbird	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )