This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ORDER THEORY Lattices Subset order structures 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 ) ) )