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 φAMooreX
mrieqvd.2 N=mrClsA
mrieqvd.3 I=mrIndA
mrieqvd.4 φSX
Assertion mrieqvd φSIxSNSxNS

Proof

Step Hyp Ref Expression
1 mrieqvd.1 φAMooreX
2 mrieqvd.2 N=mrClsA
3 mrieqvd.3 I=mrIndA
4 mrieqvd.4 φSX
5 2 3 1 4 ismri2d φSIxS¬xNSx
6 1 adantr φxSAMooreX
7 4 adantr φxSSX
8 simpr φxSxS
9 6 2 7 8 mrieqvlemd φxSxNSxNSx=NS
10 9 necon3bbid φxS¬xNSxNSxNS
11 10 ralbidva φxS¬xNSxxSNSxNS
12 5 11 bitrd φSIxSNSxNS