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	|- ( ph -> A e. ( Moore ` X ) )
	ismri2dad.4	|- ( ph -> S e. I )
	ismri2dad.5	|- ( ph -> Y e. S )
Assertion	ismri2dad	|- ( ph -> -. Y e. ( N ` ( S \ { Y } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismri2dad.1	|- N = ( mrCls ` A )
2		ismri2dad.2	|- I = ( mrInd ` A )
3		ismri2dad.3	|- ( ph -> A e. ( Moore ` X ) )
4		ismri2dad.4	|- ( ph -> S e. I )
5		ismri2dad.5	|- ( ph -> Y e. S )
6	2 3 4	mrissd	|- ( ph -> S C_ X )
7	1 2 3 6	ismri2d	|- ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
8	4 7	mpbid	|- ( ph -> A. x e. S -. x e. ( N ` ( S \ { x } ) ) )
9		simpr	|- ( ( ph /\ x = Y ) -> x = Y )
10	9	sneqd	|- ( ( ph /\ x = Y ) -> { x } = { Y } )
11	10	difeq2d	|- ( ( ph /\ x = Y ) -> ( S \ { x } ) = ( S \ { Y } ) )
12	11	fveq2d	|- ( ( ph /\ x = Y ) -> ( N ` ( S \ { x } ) ) = ( N ` ( S \ { Y } ) ) )
13	9 12	eleq12d	|- ( ( ph /\ x = Y ) -> ( x e. ( N ` ( S \ { x } ) ) <-> Y e. ( N ` ( S \ { Y } ) ) ) )
14	13	notbid	|- ( ( ph /\ x = Y ) -> ( -. x e. ( N ` ( S \ { x } ) ) <-> -. Y e. ( N ` ( S \ { Y } ) ) ) )
15	5 14	rspcdv	|- ( ph -> ( A. x e. S -. x e. ( N ` ( S \ { x } ) ) -> -. Y e. ( N ` ( S \ { Y } ) ) ) )
16	8 15	mpd	|- ( ph -> -. Y e. ( N ` ( S \ { Y } ) ) )