Theorem mrieqvlemd

Description: In a Moore system, if Y is a member of S , ( S \ { Y } ) and S have the same closure if and only if Y is in the closure of ( S \ { Y } ) . Used in the proof of mrieqvd and mrieqv2d . Deduction form. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrieqvlemd.1	|- ( ph -> A e. ( Moore ` X ) )
	mrieqvlemd.2	|- N = ( mrCls ` A )
	mrieqvlemd.3	|- ( ph -> S C_ X )
	mrieqvlemd.4	|- ( ph -> Y e. S )
Assertion	mrieqvlemd	|- ( ph -> ( Y e. ( N ` ( S \ { Y } ) ) <-> ( N ` ( S \ { Y } ) ) = ( N ` S ) ) )

Proof

Step	Hyp	Ref	Expression
1		mrieqvlemd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mrieqvlemd.2	|- N = ( mrCls ` A )
3		mrieqvlemd.3	|- ( ph -> S C_ X )
4		mrieqvlemd.4	|- ( ph -> Y e. S )
5	1	adantr	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> A e. ( Moore ` X ) )
6		undif1	|- ( ( S \ { Y } ) u. { Y } ) = ( S u. { Y } )
7	3	adantr	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> S C_ X )
8	7	ssdifssd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( S \ { Y } ) C_ X )
9	5 2 8	mrcssidd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( S \ { Y } ) C_ ( N ` ( S \ { Y } ) ) )
10		simpr	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> Y e. ( N ` ( S \ { Y } ) ) )
11	10	snssd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> { Y } C_ ( N ` ( S \ { Y } ) ) )
12	9 11	unssd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( ( S \ { Y } ) u. { Y } ) C_ ( N ` ( S \ { Y } ) ) )
13	6 12	eqsstrrid	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( S u. { Y } ) C_ ( N ` ( S \ { Y } ) ) )
14	13	unssad	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> S C_ ( N ` ( S \ { Y } ) ) )
15		difssd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( S \ { Y } ) C_ S )
16	5 2 14 15	mressmrcd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( N ` S ) = ( N ` ( S \ { Y } ) ) )
17	16	eqcomd	|- ( ( ph /\ Y e. ( N ` ( S \ { Y } ) ) ) -> ( N ` ( S \ { Y } ) ) = ( N ` S ) )
18	1 2 3	mrcssidd	|- ( ph -> S C_ ( N ` S ) )
19	18 4	sseldd	|- ( ph -> Y e. ( N ` S ) )
20	19	adantr	|- ( ( ph /\ ( N ` ( S \ { Y } ) ) = ( N ` S ) ) -> Y e. ( N ` S ) )
21		simpr	|- ( ( ph /\ ( N ` ( S \ { Y } ) ) = ( N ` S ) ) -> ( N ` ( S \ { Y } ) ) = ( N ` S ) )
22	20 21	eleqtrrd	|- ( ( ph /\ ( N ` ( S \ { Y } ) ) = ( N ` S ) ) -> Y e. ( N ` ( S \ { Y } ) ) )
23	17 22	impbida	|- ( ph -> ( Y e. ( N ` ( S \ { Y } ) ) <-> ( N ` ( S \ { Y } ) ) = ( N ` S ) ) )