Metamath Proof Explorer


Theorem mrieqvd

Description: In a Moore system, a set is independent if and only if, for all elements of the set, the closure of the set with the element removed is unequal to the closure of the original set. Part of Proposition 4.1.3 in FaureFrolicher p. 83. (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 mrieqvd.1
 |-  ( ph -> A e. ( Moore ` X ) )
2 mrieqvd.2
 |-  N = ( mrCls ` A )
3 mrieqvd.3
 |-  I = ( mrInd ` A )
4 mrieqvd.4
 |-  ( ph -> S C_ X )
5 2 3 1 4 ismri2d
 |-  ( ph -> ( S e. I <-> A. x e. S -. x e. ( N ` ( S \ { x } ) ) ) )
6 1 adantr
 |-  ( ( ph /\ x e. S ) -> A e. ( Moore ` X ) )
7 4 adantr
 |-  ( ( ph /\ x e. S ) -> S C_ X )
8 simpr
 |-  ( ( ph /\ x e. S ) -> x e. S )
9 6 2 7 8 mrieqvlemd
 |-  ( ( ph /\ x e. S ) -> ( x e. ( N ` ( S \ { x } ) ) <-> ( N ` ( S \ { x } ) ) = ( N ` S ) ) )
10 9 necon3bbid
 |-  ( ( ph /\ x e. S ) -> ( -. x e. ( N ` ( S \ { x } ) ) <-> ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) )
11 10 ralbidva
 |-  ( ph -> ( A. x e. S -. x e. ( N ` ( S \ { x } ) ) <-> A. x e. S ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) )
12 5 11 bitrd
 |-  ( ph -> ( S e. I <-> A. x e. S ( N ` ( S \ { x } ) ) =/= ( N ` S ) ) )