Metamath Proof Explorer

Theorem isnacs2

Description: Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis isnacs.f ⊢ F = mrCls ⁡ C
Assertion isnacs2 ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ F 𝒫 X ∩ Fin = C

Proof

Step Hyp Ref Expression
1 isnacs.f ⊢ F = mrCls ⁡ C
2 1 isnacs ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
3 eqcom ⊢ s = F ⁡ g ↔ F ⁡ g = s
4 3 rexbii ⊢ ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ ∃ g ∈ 𝒫 X ∩ Fin F ⁡ g = s
5 acsmre ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X
6 1 mrcf ⊢ C ∈ Moore ⁡ X → F : 𝒫 X ⟶ C
7 ffn ⊢ F : 𝒫 X ⟶ C → F Fn 𝒫 X
8 5 6 7 3syl ⊢ C ∈ ACS ⁡ X → F Fn 𝒫 X
9 inss1 ⊢ 𝒫 X ∩ Fin ⊆ 𝒫 X
10 fvelimab ⊢ F Fn 𝒫 X ∧ 𝒫 X ∩ Fin ⊆ 𝒫 X → s ∈ F 𝒫 X ∩ Fin ↔ ∃ g ∈ 𝒫 X ∩ Fin F ⁡ g = s
11 8 9 10 sylancl ⊢ C ∈ ACS ⁡ X → s ∈ F 𝒫 X ∩ Fin ↔ ∃ g ∈ 𝒫 X ∩ Fin F ⁡ g = s
12 4 11 bitr4id ⊢ C ∈ ACS ⁡ X → ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ s ∈ F 𝒫 X ∩ Fin
13 12 ralbidv ⊢ C ∈ ACS ⁡ X → ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ ∀ s ∈ C s ∈ F 𝒫 X ∩ Fin
14 dfss3 ⊢ C ⊆ F 𝒫 X ∩ Fin ↔ ∀ s ∈ C s ∈ F 𝒫 X ∩ Fin
15 13 14 bitr4di ⊢ C ∈ ACS ⁡ X → ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ C ⊆ F 𝒫 X ∩ Fin
16 imassrn ⊢ F 𝒫 X ∩ Fin ⊆ ran ⁡ F
17 frn ⊢ F : 𝒫 X ⟶ C → ran ⁡ F ⊆ C
18 5 6 17 3syl ⊢ C ∈ ACS ⁡ X → ran ⁡ F ⊆ C
19 16 18 sstrid ⊢ C ∈ ACS ⁡ X → F 𝒫 X ∩ Fin ⊆ C
20 19 biantrurd ⊢ C ∈ ACS ⁡ X → C ⊆ F 𝒫 X ∩ Fin ↔ F 𝒫 X ∩ Fin ⊆ C ∧ C ⊆ F 𝒫 X ∩ Fin
21 eqss ⊢ F 𝒫 X ∩ Fin = C ↔ F 𝒫 X ∩ Fin ⊆ C ∧ C ⊆ F 𝒫 X ∩ Fin
22 20 21 bitr4di ⊢ C ∈ ACS ⁡ X → C ⊆ F 𝒫 X ∩ Fin ↔ F 𝒫 X ∩ Fin = C
23 15 22 bitrd ⊢ C ∈ ACS ⁡ X → ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ F 𝒫 X ∩ Fin = C
24 23 pm5.32i ⊢ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ C ∈ ACS ⁡ X ∧ F 𝒫 X ∩ Fin = C
25 2 24 bitri ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ F 𝒫 X ∩ Fin = C