Theorem ismri

Description: Criterion for a set to be an independent set of a Moore system. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	ismri.1	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	ismri.2	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
Assertion	ismri	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ismri.1	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
2		ismri.2	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
3	1 2	mrisval	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝐼 = { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } )
4	3	eleq2d	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } ) )
5		difeq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∖ { 𝑥 } ) = ( 𝑆 ∖ { 𝑥 } ) )
6	5	fveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) = ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
7	6	eleq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
8	7	notbid	⊢ ( 𝑠 = 𝑆 → ( ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
9	8	raleqbi1dv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) ↔ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
10	9	elrab	⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝑋 ∣ ∀ 𝑥 ∈ 𝑠 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑠 ∖ { 𝑥 } ) ) } ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
11	4 10	bitrdi	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
12		elfvex	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ V )
13		elpw2g	⊢ ( 𝑋 ∈ V → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
14	12 13	syl	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝒫 𝑋 ↔ 𝑆 ⊆ 𝑋 ) )
15	14	anbi1d	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( ( 𝑆 ∈ 𝒫 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
16	11 15	bitrd	⊢ ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( 𝑆 ∈ 𝐼 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑥 ∈ 𝑆 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )