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 e. ( NoeACS ` X ) /\ S e. C ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )

Proof

Step	Hyp	Ref	Expression
1		isnacs.f	|- F = ( mrCls ` C )
2	1	isnacs	|- ( C e. ( NoeACS ` X ) <-> ( C e. ( ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) )
3	2	simprbi	|- ( C e. ( NoeACS ` X ) -> A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) )
4		eqeq1	|- ( s = S -> ( s = ( F ` g ) <-> S = ( F ` g ) ) )
5	4	rexbidv	|- ( s = S -> ( E. g e. ( ~P X i^i Fin ) s = ( F ` g ) <-> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) ) )
6	5	rspcva	|- ( ( S e. C /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )
7	3 6	sylan2	|- ( ( S e. C /\ C e. ( NoeACS ` X ) ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )
8	7	ancoms	|- ( ( C e. ( NoeACS ` X ) /\ S e. C ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )