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 ⊢ φ → A ∈ ACS ⁡ X
acsficld.2 ⊢ N = mrCls ⁡ A
acsficld.3 ⊢ φ → S ⊆ X
Assertion acsficl2d ⊢ φ → Y ∈ N ⁡ S ↔ ∃ x ∈ 𝒫 S ∩ Fin Y ∈ N ⁡ x

Proof

Step Hyp Ref Expression
1 acsficld.1 ⊢ φ → A ∈ ACS ⁡ X
2 acsficld.2 ⊢ N = mrCls ⁡ A
3 acsficld.3 ⊢ φ → S ⊆ X
4 1 2 3 acsficld ⊢ φ → N ⁡ S = ⋃ N 𝒫 S ∩ Fin
5 4 eleq2d ⊢ φ → Y ∈ N ⁡ S ↔ Y ∈ ⋃ N 𝒫 S ∩ Fin
6 1 acsmred ⊢ φ → A ∈ Moore ⁡ X
7 funmpt ⊢ Fun ⁡ z ∈ 𝒫 X ⟼ ⋂ w ∈ A | z ⊆ w
8 2 mrcfval ⊢ A ∈ Moore ⁡ X → N = z ∈ 𝒫 X ⟼ ⋂ w ∈ A | z ⊆ w
9 8 funeqd ⊢ A ∈ Moore ⁡ X → Fun ⁡ N ↔ Fun ⁡ z ∈ 𝒫 X ⟼ ⋂ w ∈ A | z ⊆ w
10 7 9 mpbiri ⊢ A ∈ Moore ⁡ X → Fun ⁡ N
11 eluniima ⊢ Fun ⁡ N → Y ∈ ⋃ N 𝒫 S ∩ Fin ↔ ∃ x ∈ 𝒫 S ∩ Fin Y ∈ N ⁡ x
12 6 10 11 3syl ⊢ φ → Y ∈ ⋃ N 𝒫 S ∩ Fin ↔ ∃ x ∈ 𝒫 S ∩ Fin Y ∈ N ⁡ x
13 5 12 bitrd ⊢ φ → Y ∈ N ⁡ S ↔ ∃ x ∈ 𝒫 S ∩ Fin Y ∈ N ⁡ x