Database
BASIC ORDER THEORY
Posets and lattices using extensible structures
Subset order structures
acsficld
Metamath Proof Explorer
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 ) ) )