Theorem mrissmrid

Description: In a Moore system, subsets of independent sets are independent. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrissmrid.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
	mrissmrid.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	mrissmrid.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	mrissmrid.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	mrissmrid.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
Assertion	mrissmrid	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		mrissmrid.1	⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
2		mrissmrid.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		mrissmrid.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4		mrissmrid.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
5		mrissmrid.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
6	3 1 4	mrissd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
7	5 6	sstrd	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
8	2 3 1 6	ismri2d	⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
9	4 8	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
10	5	sseld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ 𝑆 ) )
11	5	ssdifd	⊢ ( 𝜑 → ( 𝑇 ∖ { 𝑥 } ) ⊆ ( 𝑆 ∖ { 𝑥 } ) )
12	6	ssdifssd	⊢ ( 𝜑 → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
13	1 2 11 12	mrcssd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝑇 ∖ { 𝑥 } ) ) ⊆ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
14	13	ssneld	⊢ ( 𝜑 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑇 ∖ { 𝑥 } ) ) ) )
15	10 14	imim12d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) → ( 𝑥 ∈ 𝑇 → ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑇 ∖ { 𝑥 } ) ) ) ) )
16	15	ralimdv2	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) → ∀ 𝑥 ∈ 𝑇 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑇 ∖ { 𝑥 } ) ) ) )
17	9 16	mpd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑇 ∖ { 𝑥 } ) ) )
18	2 3 1 7 17	ismri2dd	⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )