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	$⊢ φ \to A \in ACS (X)$
		acsficld.2	$⊢ N = mrCls (A)$
		acsficld.3	$⊢ φ \to S \subseteq X$
	Assertion	acsficl2d	$⊢ φ \to (Y \in N (S) \leftrightarrow \exists x \in (𝒫 S \cap Fin) Y \in N (x))$

Proof

Step	Hyp	Ref	Expression
1		acsficld.1	$⊢ φ \to A \in ACS (X)$
2		acsficld.2	$⊢ N = mrCls (A)$
3		acsficld.3	$⊢ φ \to S \subseteq X$
4	1 2 3	acsficld	$⊢ φ \to N (S) = ⋃ N [𝒫 S \cap Fin]$
5	4	eleq2d	$⊢ φ \to (Y \in N (S) \leftrightarrow Y \in ⋃ N [𝒫 S \cap Fin])$
6	1	acsmred	$⊢ φ \to A \in Moore (X)$
7		funmpt	$⊢ Fun (z \in 𝒫 X ⟼ ⋂ \{w \in A \| z \subseteq w\})$
8	2	mrcfval	$⊢ A \in Moore (X) \to N = (z \in 𝒫 X ⟼ ⋂ \{w \in A \| z \subseteq w\})$
9	8	funeqd	$⊢ A \in Moore (X) \to (Fun N \leftrightarrow Fun (z \in 𝒫 X ⟼ ⋂ \{w \in A \| z \subseteq w\}))$
10	7 9	mpbiri	$⊢ A \in Moore (X) \to Fun N$
11		eluniima	$⊢ Fun N \to (Y \in ⋃ N [𝒫 S \cap Fin] \leftrightarrow \exists x \in (𝒫 S \cap Fin) Y \in N (x))$
12	6 10 11	3syl	$⊢ φ \to (Y \in ⋃ N [𝒫 S \cap Fin] \leftrightarrow \exists x \in (𝒫 S \cap Fin) Y \in N (x))$
13	5 12	bitrd	$⊢ φ \to (Y \in N (S) \leftrightarrow \exists x \in (𝒫 S \cap Fin) Y \in N (x))$