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

Metamath Proof Explorer

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 ) ) )