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	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	nacsfg	⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		isnacs.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	isnacs	⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ↔ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ) )
3	2	simprbi	⊢ ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) )
4		eqeq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ 𝑆 = ( 𝐹 ‘ 𝑔 ) ) )
5	4	rexbidv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ↔ ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) ) )
6	5	rspcva	⊢ ( ( 𝑆 ∈ 𝐶 ∧ ∀ 𝑠 ∈ 𝐶 ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑠 = ( 𝐹 ‘ 𝑔 ) ) → ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) )
7	3 6	sylan2	⊢ ( ( 𝑆 ∈ 𝐶 ∧ 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ) → ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) )
8	7	ancoms	⊢ ( ( 𝐶 ∈ ( NoeACS ‘ 𝑋 ) ∧ 𝑆 ∈ 𝐶 ) → ∃ 𝑔 ∈ ( 𝒫 𝑋 ∩ Fin ) 𝑆 = ( 𝐹 ‘ 𝑔 ) )