isacs4lem

Description: In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		acsdrscl.f	$⊢ F = mrCls (C)$
2		simpll	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to C \in Moore (X)$
3		elpwi	$⊢ t \in 𝒫 𝒫 X \to t \subseteq 𝒫 X$
4	3	ad2antrl	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to t \subseteq 𝒫 X$
5	1	mrcuni	$⊢ (C \in Moore (X) \land t \subseteq 𝒫 X) \to F (⋃ t) = F (⋃ F [t])$
6	2 4 5	syl2anc	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F (⋃ t) = F (⋃ F [t])$
7	1	mrcf	$⊢ C \in Moore (X) \to F : 𝒫 X ⟶ C$
8	7	ffnd	$⊢ C \in Moore (X) \to F Fn 𝒫 X$
9	8	adantr	$⊢ (C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F Fn 𝒫 X$
10		simpll	$⊢ ((C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \land (x \subseteq y \land y \subseteq X)) \to C \in Moore (X)$
11		simprl	$⊢ ((C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \land (x \subseteq y \land y \subseteq X)) \to x \subseteq y$
12		simprr	$⊢ ((C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \land (x \subseteq y \land y \subseteq X)) \to y \subseteq X$
13	10 1 11 12	mrcssd	$⊢ ((C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \land (x \subseteq y \land y \subseteq X)) \to F (x) \subseteq F (y)$
14		simprr	$⊢ (C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to toInc (t) \in Dirset$
15	3	ad2antrl	$⊢ (C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to t \subseteq 𝒫 X$
16	1	fvexi	$⊢ F \in V$
17	16	imaex	$⊢ F [t] \in V$
18	17	a1i	$⊢ (C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F [t] \in V$
19	9 13 14 15 18	ipodrsima	$⊢ (C \in Moore (X) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to toInc (F [t]) \in Dirset$
20	19	adantlr	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to toInc (F [t]) \in Dirset$
21		fveq2	$⊢ s = F [t] \to toInc (s) = toInc (F [t])$
22	21	eleq1d	$⊢ s = F [t] \to (toInc (s) \in Dirset \leftrightarrow toInc (F [t]) \in Dirset)$
23		unieq	$⊢ s = F [t] \to ⋃ s = ⋃ F [t]$
24	23	eleq1d	$⊢ s = F [t] \to (⋃ s \in C \leftrightarrow ⋃ F [t] \in C)$
25	22 24	imbi12d	$⊢ s = F [t] \to ((toInc (s) \in Dirset \to ⋃ s \in C) \leftrightarrow (toInc (F [t]) \in Dirset \to ⋃ F [t] \in C))$
26		simplr	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)$
27		imassrn	$⊢ F [t] \subseteq ran F$
28	7	frnd	$⊢ C \in Moore (X) \to ran F \subseteq C$
29	27 28	sstrid	$⊢ C \in Moore (X) \to F [t] \subseteq C$
30	17	elpw	$⊢ F [t] \in 𝒫 C \leftrightarrow F [t] \subseteq C$
31	29 30	sylibr	$⊢ C \in Moore (X) \to F [t] \in 𝒫 C$
32	31	ad2antrr	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F [t] \in 𝒫 C$
33	25 26 32	rspcdva	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to (toInc (F [t]) \in Dirset \to ⋃ F [t] \in C)$
34	20 33	mpd	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to ⋃ F [t] \in C$
35	1	mrcid	$⊢ (C \in Moore (X) \land ⋃ F [t] \in C) \to F (⋃ F [t]) = ⋃ F [t]$
36	2 34 35	syl2anc	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F (⋃ F [t]) = ⋃ F [t]$
37	6 36	eqtrd	$⊢ ((C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \land (t \in 𝒫 𝒫 X \land toInc (t) \in Dirset)) \to F (⋃ t) = ⋃ F [t]$
38	37	exp32	$⊢ (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \to (t \in 𝒫 𝒫 X \to (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t]))$
39	38	ralrimiv	$⊢ (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)) \to \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t])$
40	39	ex	$⊢ C \in Moore (X) \to (\forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C) \to \forall t \in 𝒫 𝒫 X (toInc (t) \in Dirset \to F (⋃ t) = ⋃ F [t]))$
41	40	imdistani	$⊢ (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]))$

Metamath Proof Explorer

Theorem isacs4lem

Proof