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∩Fins=F⁡g
3 eqcom ⊢s=F⁡g↔F⁡g=s
4 3 rexbii ⊢∃g∈𝒫X∩Fins=F⁡g↔∃g∈𝒫X∩FinF⁡g=s
5 acsmre ⊢C∈ACS⁡X→C∈Moore⁡X
6 1 mrcf ⊢C∈Moore⁡X→F:𝒫X⟶C
7 ffn ⊢F:𝒫X⟶C→FFn𝒫X
8 5 6 7 3syl ⊢C∈ACS⁡X→FFn𝒫X
9 inss1 ⊢𝒫X∩Fin⊆𝒫X
10 fvelimab ⊢FFn𝒫X∧𝒫X∩Fin⊆𝒫X→s∈F𝒫X∩Fin↔∃g∈𝒫X∩FinF⁡g=s
11 8 9 10 sylancl ⊢C∈ACS⁡X→s∈F𝒫X∩Fin↔∃g∈𝒫X∩FinF⁡g=s
12 4 11 bitr4id ⊢C∈ACS⁡X→∃g∈𝒫X∩Fins=F⁡g↔s∈F𝒫X∩Fin
13 12 ralbidv ⊢C∈ACS⁡X→∀s∈C∃g∈𝒫X∩Fins=F⁡g↔∀s∈Cs∈F𝒫X∩Fin
14 dfss3 ⊢C⊆F𝒫X∩Fin↔∀s∈Cs∈F𝒫X∩Fin
15 13 14 bitr4di ⊢C∈ACS⁡X→∀s∈C∃g∈𝒫X∩Fins=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∩Fins=F⁡g↔F𝒫X∩Fin=C
24 23 pm5.32i ⊢C∈ACS⁡X∧∀s∈C∃g∈𝒫X∩Fins=F⁡g↔C∈ACS⁡X∧F𝒫X∩Fin=C
25 2 24 bitri ⊢C∈NoeACS⁡X↔C∈ACS⁡X∧F𝒫X∩Fin=C