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 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
ismri2dad.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
ismri2dad.3 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
ismri2dad.4 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
ismri2dad.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion ismri2dad ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )

Proof

Step Hyp Ref Expression
1 ismri2dad.1 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
2 ismri2dad.2 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
3 ismri2dad.3 ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
4 ismri2dad.4 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
5 ismri2dad.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
6 2 3 4 mrissd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
7 1 2 3 6 ismri2d ⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
8 4 7 mpbid ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
10 9 sneqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → { 𝑥 } = { 𝑌 } )
11 10 difeq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑆 ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑌 } ) )
12 11 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )
13 9 12 eleq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) )
14 13 notbid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ¬ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) )
15 5 14 rspcdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) ) )
16 8 15 mpd ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )