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

Metamath Proof Explorer

Theorem acsfiel2

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 3-Apr-2015)

		Ref	Expression
	Hypothesis	isacs2.f	$⊢ F = mrCls (C)$
	Assertion	acsfiel2	$⊢ (C \in ACS (X) \land S \subseteq X) \to (S \in C \leftrightarrow \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S)$

Proof

Step	Hyp	Ref	Expression
1		isacs2.f	$⊢ F = mrCls (C)$
2	1	acsfiel	$⊢ C \in ACS (X) \to (S \in C \leftrightarrow (S \subseteq X \land \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S))$
3	2	baibd	$⊢ (C \in ACS (X) \land S \subseteq X) \to (S \in C \leftrightarrow \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S)$