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 ⊢ φ → A ∈ Moore ⁡ X
mrissmrid.2 ⊢ N = mrCls ⁡ A
mrissmrid.3 ⊢ I = mrInd ⁡ A
mrissmrid.4 ⊢ φ → S ∈ I
mrissmrid.5 ⊢ φ → T ⊆ S
Assertion mrissmrid ⊢ φ → T ∈ I

Proof

Step Hyp Ref Expression
1 mrissmrid.1 ⊢ φ → A ∈ Moore ⁡ X
2 mrissmrid.2 ⊢ N = mrCls ⁡ A
3 mrissmrid.3 ⊢ I = mrInd ⁡ A
4 mrissmrid.4 ⊢ φ → S ∈ I
5 mrissmrid.5 ⊢ φ → T ⊆ S
6 3 1 4 mrissd ⊢ φ → S ⊆ X
7 5 6 sstrd ⊢ φ → T ⊆ X
8 2 3 1 6 ismri2d ⊢ φ → S ∈ I ↔ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
9 4 8 mpbid ⊢ φ → ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
10 5 sseld ⊢ φ → x ∈ T → x ∈ S
11 5 ssdifd ⊢ φ → T ∖ x ⊆ S ∖ x
12 6 ssdifssd ⊢ φ → S ∖ x ⊆ X
13 1 2 11 12 mrcssd ⊢ φ → N ⁡ T ∖ x ⊆ N ⁡ S ∖ x
14 13 ssneld ⊢ φ → ¬ x ∈ N ⁡ S ∖ x → ¬ x ∈ N ⁡ T ∖ x
15 10 14 imim12d ⊢ φ → x ∈ S → ¬ x ∈ N ⁡ S ∖ x → x ∈ T → ¬ x ∈ N ⁡ T ∖ x
16 15 ralimdv2 ⊢ φ → ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x → ∀ x ∈ T ¬ x ∈ N ⁡ T ∖ x
17 9 16 mpd ⊢ φ → ∀ x ∈ T ¬ x ∈ N ⁡ T ∖ x
18 2 3 1 7 17 ismri2dd ⊢ φ → T ∈ I