This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) 𝑌 ∈ ( 𝑁 ‘ 𝑥 ) ) )