Metamath Proof Explorer

Theorem isnacs

Description: Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 isnacs.f ⊢ F = mrCls ⁡ C
2 elfvex ⊢ C ∈ NoeACS ⁡ X → X ∈ V
3 elfvex ⊢ C ∈ ACS ⁡ X → X ∈ V
4 3 adantr ⊢ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g → X ∈ V
5 fveq2 ⊢ x = X → ACS ⁡ x = ACS ⁡ X
6 pweq ⊢ x = X → 𝒫 x = 𝒫 X
7 6 ineq1d ⊢ x = X → 𝒫 x ∩ Fin = 𝒫 X ∩ Fin
8 7 rexeqdv ⊢ x = X → ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g ↔ ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g
9 8 ralbidv ⊢ x = X → ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g ↔ ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g
10 5 9 rabeqbidv ⊢ x = X → c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g = c ∈ ACS ⁡ X | ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g
11 df-nacs ⊢ NoeACS = x ∈ V ⟼ c ∈ ACS ⁡ x | ∀ s ∈ c ∃ g ∈ 𝒫 x ∩ Fin s = mrCls ⁡ c ⁡ g
12 fvex ⊢ ACS ⁡ X ∈ V
13 12 rabex ⊢ c ∈ ACS ⁡ X | ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g ∈ V
14 10 11 13 fvmpt ⊢ X ∈ V → NoeACS ⁡ X = c ∈ ACS ⁡ X | ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g
15 14 eleq2d ⊢ X ∈ V → C ∈ NoeACS ⁡ X ↔ C ∈ c ∈ ACS ⁡ X | ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g
16 fveq2 ⊢ c = C → mrCls ⁡ c = mrCls ⁡ C
17 16 1 eqtr4di ⊢ c = C → mrCls ⁡ c = F
18 17 fveq1d ⊢ c = C → mrCls ⁡ c ⁡ g = F ⁡ g
19 18 eqeq2d ⊢ c = C → s = mrCls ⁡ c ⁡ g ↔ s = F ⁡ g
20 19 rexbidv ⊢ c = C → ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g ↔ ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
21 20 raleqbi1dv ⊢ c = C → ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g ↔ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
22 21 elrab ⊢ C ∈ c ∈ ACS ⁡ X | ∀ s ∈ c ∃ g ∈ 𝒫 X ∩ Fin s = mrCls ⁡ c ⁡ g ↔ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
23 15 22 bitrdi ⊢ X ∈ V → C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g
24 2 4 23 pm5.21nii ⊢ C ∈ NoeACS ⁡ X ↔ C ∈ ACS ⁡ X ∧ ∀ s ∈ C ∃ g ∈ 𝒫 X ∩ Fin s = F ⁡ g