acsdrsel

Description: An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015)

		Ref	Expression
	Assertion	acsdrsel	$⊢ (C \in ACS (X) \land Y \subseteq C \land toInc (Y) \in Dirset) \to ⋃ Y \in C$

Step	Hyp	Ref	Expression
1		fveq2	$⊢ s = Y \to toInc (s) = toInc (Y)$
2	1	eleq1d	$⊢ s = Y \to (toInc (s) \in Dirset \leftrightarrow toInc (Y) \in Dirset)$
3		unieq	$⊢ s = Y \to ⋃ s = ⋃ Y$
4	3	eleq1d	$⊢ s = Y \to (⋃ s \in C \leftrightarrow ⋃ Y \in C)$
5	2 4	imbi12d	$⊢ s = Y \to ((toInc (s) \in Dirset \to ⋃ s \in C) \leftrightarrow (toInc (Y) \in Dirset \to ⋃ Y \in C))$
6		isacs3lem	$⊢ C \in ACS (X) \to (C \in Moore (X) \land \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C))$
7	6	simprd	$⊢ C \in ACS (X) \to \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)$
8	7	adantr	$⊢ (C \in ACS (X) \land Y \subseteq C) \to \forall s \in 𝒫 C (toInc (s) \in Dirset \to ⋃ s \in C)$
9		elpw2g	$⊢ C \in ACS (X) \to (Y \in 𝒫 C \leftrightarrow Y \subseteq C)$
10	9	biimpar	$⊢ (C \in ACS (X) \land Y \subseteq C) \to Y \in 𝒫 C$
11	5 8 10	rspcdva	$⊢ (C \in ACS (X) \land Y \subseteq C) \to (toInc (Y) \in Dirset \to ⋃ Y \in C)$
12	11	3impia	$⊢ (C \in ACS (X) \land Y \subseteq C \land toInc (Y) \in Dirset) \to ⋃ Y \in C$

Metamath Proof Explorer