# 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 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
mrieqvd.2 𝑁 = ( mrCls ‘ 𝐴 )
mrieqvd.3 𝐼 = ( mrInd ‘ 𝐴 )
mrieqvd.4 ( 𝜑𝑆𝑋 )
Assertion mrieqvd ( 𝜑 → ( 𝑆𝐼 ↔ ∀ 𝑥𝑆 ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁𝑆 ) ) )

### Proof

Step Hyp Ref Expression
1 mrieqvd.1 ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
2 mrieqvd.2 𝑁 = ( mrCls ‘ 𝐴 )
3 mrieqvd.3 𝐼 = ( mrInd ‘ 𝐴 )
4 mrieqvd.4 ( 𝜑𝑆𝑋 )
5 2 3 1 4 ismri2d ( 𝜑 → ( 𝑆𝐼 ↔ ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
6 1 adantr ( ( 𝜑𝑥𝑆 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
7 4 adantr ( ( 𝜑𝑥𝑆 ) → 𝑆𝑋 )
8 simpr ( ( 𝜑𝑥𝑆 ) → 𝑥𝑆 )
9 6 2 7 8 mrieqvlemd ( ( 𝜑𝑥𝑆 ) → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( 𝑁𝑆 ) ) )
10 9 necon3bbid ( ( 𝜑𝑥𝑆 ) → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁𝑆 ) ) )
11 10 ralbidva ( 𝜑 → ( ∀ 𝑥𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥𝑆 ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁𝑆 ) ) )
12 5 11 bitrd ( 𝜑 → ( 𝑆𝐼 ↔ ∀ 𝑥𝑆 ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁𝑆 ) ) )