Metamath Proof Explorer


Theorem acsficl2d

Description: In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl . Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsficld.1 ( 𝜑𝐴 ∈ ( ACS ‘ 𝑋 ) )
acsficld.2 𝑁 = ( mrCls ‘ 𝐴 )
acsficld.3 ( 𝜑𝑆𝑋 )
Assertion acsficl2d ( 𝜑 → ( 𝑌 ∈ ( 𝑁𝑆 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 acsficld.1 ( 𝜑𝐴 ∈ ( ACS ‘ 𝑋 ) )
2 acsficld.2 𝑁 = ( mrCls ‘ 𝐴 )
3 acsficld.3 ( 𝜑𝑆𝑋 )
4 1 2 3 acsficld ( 𝜑 → ( 𝑁𝑆 ) = ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) )
5 4 eleq2d ( 𝜑 → ( 𝑌 ∈ ( 𝑁𝑆 ) ↔ 𝑌 ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ) )
6 1 acsmred ( 𝜑𝐴 ∈ ( Moore ‘ 𝑋 ) )
7 funmpt Fun ( 𝑧 ∈ 𝒫 𝑋 { 𝑤𝐴𝑧𝑤 } )
8 2 mrcfval ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → 𝑁 = ( 𝑧 ∈ 𝒫 𝑋 { 𝑤𝐴𝑧𝑤 } ) )
9 8 funeqd ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → ( Fun 𝑁 ↔ Fun ( 𝑧 ∈ 𝒫 𝑋 { 𝑤𝐴𝑧𝑤 } ) ) )
10 7 9 mpbiri ( 𝐴 ∈ ( Moore ‘ 𝑋 ) → Fun 𝑁 )
11 eluniima ( Fun 𝑁 → ( 𝑌 ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁𝑥 ) ) )
12 6 10 11 3syl ( 𝜑 → ( 𝑌 ( 𝑁 “ ( 𝒫 𝑆 ∩ Fin ) ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁𝑥 ) ) )
13 5 12 bitrd ( 𝜑 → ( 𝑌 ∈ ( 𝑁𝑆 ) ↔ ∃ 𝑥 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑌 ∈ ( 𝑁𝑥 ) ) )