acsfiel

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

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

Proof

Step	Hyp	Ref	Expression
1		isacs2.f	$⊢ F = mrCls (C)$
2		acsmre	$⊢ C \in ACS (X) \to C \in Moore (X)$
3		mress	$⊢ (C \in Moore (X) \land S \in C) \to S \subseteq X$
4	2 3	sylan	$⊢ (C \in ACS (X) \land S \in C) \to S \subseteq X$
5	4	ex	$⊢ C \in ACS (X) \to (S \in C \to S \subseteq X)$
6	5	pm4.71rd	$⊢ C \in ACS (X) \to (S \in C \leftrightarrow (S \subseteq X \land S \in C))$
7		eleq1	$⊢ s = S \to (s \in C \leftrightarrow S \in C)$
8		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
9	8	ineq1d	$⊢ s = S \to 𝒫 s \cap Fin = 𝒫 S \cap Fin$
10		sseq2	$⊢ s = S \to (F (y) \subseteq s \leftrightarrow F (y) \subseteq S)$
11	9 10	raleqbidv	$⊢ s = S \to (\forall y \in (𝒫 s \cap Fin) F (y) \subseteq s \leftrightarrow \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S)$
12	7 11	bibi12d	$⊢ s = S \to ((s \in C \leftrightarrow \forall y \in (𝒫 s \cap Fin) F (y) \subseteq s) \leftrightarrow (S \in C \leftrightarrow \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S))$
13	1	isacs2	$⊢ C \in ACS (X) \leftrightarrow (C \in Moore (X) \land \forall s \in 𝒫 X (s \in C \leftrightarrow \forall y \in (𝒫 s \cap Fin) F (y) \subseteq s))$
14	13	simprbi	$⊢ C \in ACS (X) \to \forall s \in 𝒫 X (s \in C \leftrightarrow \forall y \in (𝒫 s \cap Fin) F (y) \subseteq s)$
15	14	adantr	$⊢ (C \in ACS (X) \land S \subseteq X) \to \forall s \in 𝒫 X (s \in C \leftrightarrow \forall y \in (𝒫 s \cap Fin) F (y) \subseteq s)$
16		elfvdm	$⊢ C \in ACS (X) \to X \in dom ACS$
17		elpw2g	$⊢ X \in dom ACS \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
18	16 17	syl	$⊢ C \in ACS (X) \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
19	18	biimpar	$⊢ (C \in ACS (X) \land S \subseteq X) \to S \in 𝒫 X$
20	12 15 19	rspcdva	$⊢ (C \in ACS (X) \land S \subseteq X) \to (S \in C \leftrightarrow \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S)$
21	20	pm5.32da	$⊢ C \in ACS (X) \to ((S \subseteq X \land S \in C) \leftrightarrow (S \subseteq X \land \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S))$
22	6 21	bitrd	$⊢ C \in ACS (X) \to (S \in C \leftrightarrow (S \subseteq X \land \forall y \in (𝒫 S \cap Fin) F (y) \subseteq S))$

Metamath Proof Explorer

Theorem acsfiel

Proof