Metamath Proof Explorer

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 ⊢ N = mrCls ⁡ A
ismri.2 ⊢ I = mrInd ⁡ A
Assertion ismri ⊢ A ∈ Moore ⁡ X → S ∈ I ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x

Proof

Step Hyp Ref Expression
1 ismri.1 ⊢ N = mrCls ⁡ A
2 ismri.2 ⊢ I = mrInd ⁡ A
3 1 2 mrisval ⊢ A ∈ Moore ⁡ X → I = s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
4 3 eleq2d ⊢ A ∈ Moore ⁡ X → S ∈ I ↔ S ∈ s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x
5 difeq1 ⊢ s = S → s ∖ x = S ∖ x
6 5 fveq2d ⊢ s = S → N ⁡ s ∖ x = N ⁡ S ∖ x
7 6 eleq2d ⊢ s = S → x ∈ N ⁡ s ∖ x ↔ x ∈ N ⁡ S ∖ x
8 7 notbid ⊢ s = S → ¬ x ∈ N ⁡ s ∖ x ↔ ¬ x ∈ N ⁡ S ∖ x
9 8 raleqbi1dv ⊢ s = S → ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x ↔ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
10 9 elrab ⊢ S ∈ s ∈ 𝒫 X | ∀ x ∈ s ¬ x ∈ N ⁡ s ∖ x ↔ S ∈ 𝒫 X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
11 4 10 bitrdi ⊢ A ∈ Moore ⁡ X → S ∈ I ↔ S ∈ 𝒫 X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
12 elfvex ⊢ A ∈ Moore ⁡ X → X ∈ V
13 elpw2g ⊢ X ∈ V → S ∈ 𝒫 X ↔ S ⊆ X
14 12 13 syl ⊢ A ∈ Moore ⁡ X → S ∈ 𝒫 X ↔ S ⊆ X
15 14 anbi1d ⊢ A ∈ Moore ⁡ X → S ∈ 𝒫 X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x
16 11 15 bitrd ⊢ A ∈ Moore ⁡ X → S ∈ I ↔ S ⊆ X ∧ ∀ x ∈ S ¬ x ∈ N ⁡ S ∖ x