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∩Fins=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∩Fins=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∩Fins=mrCls⁡c⁡g↔∃g∈𝒫X∩Fins=mrCls⁡c⁡g
9 8 ralbidv ⊢x=X→∀s∈c∃g∈𝒫x∩Fins=mrCls⁡c⁡g↔∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g
10 5 9 rabeqbidv ⊢x=X→c∈ACS⁡x|∀s∈c∃g∈𝒫x∩Fins=mrCls⁡c⁡g=c∈ACS⁡X|∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g
11 df-nacs ⊢NoeACS=x∈V⟼c∈ACS⁡x|∀s∈c∃g∈𝒫x∩Fins=mrCls⁡c⁡g
12 fvex ⊢ACS⁡X∈V
13 12 rabex ⊢c∈ACS⁡X|∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g∈V
14 10 11 13 fvmpt ⊢X∈V→NoeACS⁡X=c∈ACS⁡X|∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g
15 14 eleq2d ⊢X∈V→C∈NoeACS⁡X↔C∈c∈ACS⁡X|∀s∈c∃g∈𝒫X∩Fins=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∩Fins=mrCls⁡c⁡g↔∃g∈𝒫X∩Fins=F⁡g
21 20 raleqbi1dv ⊢c=C→∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g↔∀s∈C∃g∈𝒫X∩Fins=F⁡g
22 21 elrab ⊢C∈c∈ACS⁡X|∀s∈c∃g∈𝒫X∩Fins=mrCls⁡c⁡g↔C∈ACS⁡X∧∀s∈C∃g∈𝒫X∩Fins=F⁡g
23 15 22 bitrdi ⊢X∈V→C∈NoeACS⁡X↔C∈ACS⁡X∧∀s∈C∃g∈𝒫X∩Fins=F⁡g
24 2 4 23 pm5.21nii ⊢C∈NoeACS⁡X↔C∈ACS⁡X∧∀s∈C∃g∈𝒫X∩Fins=F⁡g