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	⊢ ( 𝜑 → ( 𝑆 ∈ 𝐼 ↔ ∀ 𝑥 ∈ 𝑆 ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ≠ ( 𝑁 ‘ 𝑆 ) ) )