isacs5lem

Description: If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Hypothesis	acsdrscl.f	$⊢ F = mrCls (C)$
	Assertion	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])$

Proof

Step	Hyp	Ref	Expression
1		acsdrscl.f	$⊢ F = mrCls (C)$
2		unifpw	$⊢ ⋃ (𝒫 s \cap Fin) = s$
3	2	fveq2i	$⊢ F (⋃ (𝒫 s \cap Fin)) = F (s)$
4		vex	$⊢ s \in V$
5		fpwipodrs	$⊢ s \in V \to toInc (𝒫 s \cap Fin) \in Dirset$
6	4 5	mp1i	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to toInc (𝒫 s \cap Fin) \in Dirset$
7		fveq2	$⊢ t = 𝒫 s \cap Fin \to toInc (t) = toInc (𝒫 s \cap Fin)$
8	7	eleq1d	$⊢ t = 𝒫 s \cap Fin \to (toInc (t) \in Dirset \leftrightarrow toInc (𝒫 s \cap Fin) \in Dirset)$
9		unieq	$⊢ t = 𝒫 s \cap Fin \to ⋃ t = ⋃ (𝒫 s \cap Fin)$
10	9	fveq2d	$⊢ t = 𝒫 s \cap Fin \to F (⋃ t) = F (⋃ (𝒫 s \cap Fin))$
11		imaeq2	$⊢ t = 𝒫 s \cap Fin \to F [t] = F [𝒫 s \cap Fin]$
12	11	unieqd	$⊢ t = 𝒫 s \cap Fin \to ⋃ F [t] = ⋃ F [𝒫 s \cap Fin]$
13	10 12	eqeq12d	$⊢ t = 𝒫 s \cap Fin \to (F (⋃ t) = ⋃ F [t] \leftrightarrow F (⋃ (𝒫 s \cap Fin)) = ⋃ F [𝒫 s \cap Fin])$
14	8 13	imbi12d	$⊢ t = 𝒫 s \cap Fin \to ((toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t]) \leftrightarrow (toInc (𝒫 s \cap Fin) \in Dirset \to F (⋃ (𝒫 s \cap Fin)) = ⋃ F [𝒫 s \cap Fin]))$
15		simplr	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])$
16		inss1	$⊢ 𝒫 s \cap Fin \subseteq 𝒫 s$
17		elpwi	$⊢ s \in 𝒫 X \to s \subseteq X$
18	17	sspwd	$⊢ s \in 𝒫 X \to 𝒫 s \subseteq 𝒫 X$
19	18	adantl	$⊢ (C \in Moore (X) \land s \in 𝒫 X) \to 𝒫 s \subseteq 𝒫 X$
20	16 19	sstrid	$⊢ (C \in Moore (X) \land s \in 𝒫 X) \to 𝒫 s \cap Fin \subseteq 𝒫 X$
21		vpwex	$⊢ 𝒫 s \in V$
22	21	inex1	$⊢ 𝒫 s \cap Fin \in V$
23	22	elpw	$⊢ 𝒫 s \cap Fin \in 𝒫 𝒫 X \leftrightarrow 𝒫 s \cap Fin \subseteq 𝒫 X$
24	20 23	sylibr	$⊢ (C \in Moore (X) \land s \in 𝒫 X) \to 𝒫 s \cap Fin \in 𝒫 𝒫 X$
25	24	adantlr	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to 𝒫 s \cap Fin \in 𝒫 𝒫 X$
26	14 15 25	rspcdva	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to (toInc (𝒫 s \cap Fin) \in Dirset \to F (⋃ (𝒫 s \cap Fin)) = ⋃ F [𝒫 s \cap Fin])$
27	6 26	mpd	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to F (⋃ (𝒫 s \cap Fin)) = ⋃ F [𝒫 s \cap Fin]$
28	3 27	eqtr3id	$⊢ ((C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \land s \in 𝒫 X) \to F (s) = ⋃ F [𝒫 s \cap Fin]$
29	28	ralrimiva	$⊢ (C \in Moore (X) \land \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])) \to \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin]$
30	29	ex	$⊢ C \in Moore (X) \to (\forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t]) \to \forall s \in 𝒫 X F (s) = ⋃ F [𝒫 s \cap Fin])$
31	30	imdistani	$⊢ (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])$

Metamath Proof Explorer

Theorem isacs5lem

Proof