Metamath Proof Explorer

Theorem nacsfg

Description: In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Hypothesis isnacs.f ⊢ F = mrCls ⁡ C
Assertion nacsfg ⊢ C ∈ NoeACS ⁡ X ∧ S ∈ C → ∃ g ∈ 𝒫 X ∩ Fin S = F ⁡ g

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 2 simprbi ⊢ C ∈ NoeACS ⁡ X → ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
4 eqeq1 ⊢ s = S → s = F ⁡ g ↔ S = F ⁡ g
5 4 rexbidv ⊢ s = S → ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g ↔ ∃ g ∈ 𝒫 X ∩ Fin S = F ⁡ g
6 5 rspcva ⊢ S ∈ C ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g → ∃ g ∈ 𝒫 X ∩ Fin S = F ⁡ g
7 3 6 sylan2 ⊢ S ∈ C ∧ C ∈ NoeACS ⁡ X → ∃ g ∈ 𝒫 X ∩ Fin S = F ⁡ g
8 7 ancoms ⊢ C ∈ NoeACS ⁡ X ∧ S ∈ C → ∃ g ∈ 𝒫 X ∩ Fin S = F ⁡ g