Theorem acsficld

Description: In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	acsficld.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsficld.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsficld.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
Assertion	acsficld	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		acsficld.1	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2		acsficld.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3		acsficld.3	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4	2	acsficl	⊢ ( ( 𝐴 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ‘ 𝑆 ) = ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) )
5	1 3 4	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ∪ ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) )