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	⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑌 } ) ) )