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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝑇 ∈ 𝐼 )