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 \in NoeACS (X) \land S \in C) \to \exists g \in (𝒫 X \cap Fin) S = F (g)$

Step	Hyp	Ref	Expression
1		isnacs.f	$⊢ F = mrCls (C)$
2	1	isnacs	$⊢ C \in NoeACS (X) \leftrightarrow (C \in ACS (X) \land \forall s \in C \exists g \in (𝒫 X \cap Fin) s = F (g))$
3	2	simprbi	$⊢ C \in NoeACS (X) \to \forall s \in C \exists g \in (𝒫 X \cap Fin) s = F (g)$
4		eqeq1	$⊢ s = S \to (s = F (g) \leftrightarrow S = F (g))$
5	4	rexbidv	$⊢ s = S \to (\exists g \in (𝒫 X \cap Fin) s = F (g) \leftrightarrow \exists g \in (𝒫 X \cap Fin) S = F (g))$
6	5	rspcva	$⊢ (S \in C \land \forall s \in C \exists g \in (𝒫 X \cap Fin) s = F (g)) \to \exists g \in (𝒫 X \cap Fin) S = F (g)$
7	3 6	sylan2	$⊢ (S \in C \land C \in NoeACS (X)) \to \exists g \in (𝒫 X \cap Fin) S = F (g)$
8	7	ancoms	$⊢ (C \in NoeACS (X) \land S \in C) \to \exists g \in (𝒫 X \cap Fin) S = F (g)$

Metamath Proof Explorer