Metamath Proof Explorer

Theorem acsficl

Description: A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Hypothesis	acsdrscl.f	$⊢ F = mrCls (C)$
	Assertion	acsficl	$⊢ (C \in ACS (X) \land S \subseteq X) \to F (S) = ⋃ F [𝒫 S \cap Fin]$

Proof

Step	Hyp	Ref	Expression
1		acsdrscl.f	$⊢ F = mrCls (C)$
2		fveq2	$⊢ s = S \to F (s) = F (S)$
3		pweq	$⊢ s = S \to 𝒫 s = 𝒫 S$
4	3	ineq1d	$⊢ s = S \to 𝒫 s \cap Fin = 𝒫 S \cap Fin$
5	4	imaeq2d	$⊢ s = S \to F [𝒫 s \cap Fin] = F [𝒫 S \cap Fin]$
6	5	unieqd	$⊢ s = S \to ⋃ F [𝒫 s \cap Fin] = ⋃ F [𝒫 S \cap Fin]$
7	2 6	eqeq12d	$⊢ s = S \to (F (s) = ⋃ F [𝒫 s \cap Fin] \leftrightarrow F (S) = ⋃ F [𝒫 S \cap Fin])$
8		isacs3lem	$⊢ C \in ACS (X) \to (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C))$
9	1	isacs4lem	$⊢ (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \to (C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t]))$
10	1	isacs5lem	$⊢ (C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \to (C \in Moore (X) \land \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin])$
11	8 9 10	3syl	$⊢ C \in ACS (X) \to (C \in Moore (X) \land \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin])$
12	11	simprd	$⊢ C \in ACS (X) \to \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin]$
13	12	adantr	$⊢ (C \in ACS (X) \land S \subseteq X) \to \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin]$
14		elfvdm	$⊢ C \in ACS (X) \to X \in dom ACS$
15		elpw2g	$⊢ X \in dom ACS \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
16	14 15	syl	$⊢ C \in ACS (X) \to (S \in 𝒫 X \leftrightarrow S \subseteq X)$
17	16	biimpar	$⊢ (C \in ACS (X) \land S \subseteq X) \to S \in 𝒫 X$
18	7 13 17	rspcdva	$⊢ (C \in ACS (X) \land S \subseteq X) \to F (S) = ⋃ F [𝒫 S \cap Fin]$