Theorem acsfiel2

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Hypothesis	isacs2.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
Assertion	acsfiel2	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		isacs2.f	⊢ 𝐹 = ( mrCls ‘ 𝐶 )
2	1	acsfiel	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ( 𝑆 ⊆ 𝑋 ∧ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) ) )
3	2	baibd	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ 𝐶 ↔ ∀ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) ( 𝐹 ‘ 𝑦 ) ⊆ 𝑆 ) )