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

Metamath Proof Explorer

Theorem ismri2dad

Description: Consequence of a set in a Moore system being independent. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses ismri2dad.1 ⊢ N = mrCls ⁡ A
ismri2dad.2 ⊢ I = mrInd ⁡ A
ismri2dad.3 ⊢ φ → A ∈ Moore ⁡ X
ismri2dad.4 ⊢ φ → S ∈ I
ismri2dad.5 ⊢ φ → Y ∈ S
Assertion ismri2dad ⊢ φ → ¬ Y ∈ N ⁡ S ∖ Y

Proof

Step Hyp Ref Expression
1 ismri2dad.1 ⊢ N = mrCls ⁡ A
2 ismri2dad.2 ⊢ I = mrInd ⁡ A
3 ismri2dad.3 ⊢ φ → A ∈ Moore ⁡ X
4 ismri2dad.4 ⊢ φ → S ∈ I
5 ismri2dad.5 ⊢ φ → Y ∈ S
6 2 3 4 mrissd ⊢ φ → S ⊆ X
7 1 2 3 6 ismri2d ⊢ φ → S ∈ I ↔ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
8 4 7 mpbid ⊢ φ → ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
9 simpr ⊢ φ ∧ x = Y → x = Y
10 9 sneqd ⊢ φ ∧ x = Y → x = Y
11 10 difeq2d ⊢ φ ∧ x = Y → S ∖ x = S ∖ Y
12 11 fveq2d ⊢ φ ∧ x = Y → N ⁡ S ∖ x = N ⁡ S ∖ Y
13 9 12 eleq12d ⊢ φ ∧ x = Y → x ∈ N ⁡ S ∖ x ↔ Y ∈ N ⁡ S ∖ Y
14 13 notbid ⊢ φ ∧ x = Y → ¬ x ∈ N ⁡ S ∖ x ↔ ¬ Y ∈ N ⁡ S ∖ Y
15 5 14 rspcdv ⊢ φ → ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x → ¬ Y ∈ N ⁡ S ∖ Y
16 8 15 mpd ⊢ φ → ¬ Y ∈ N ⁡ S ∖ Y