Theorem 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	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ∪ 𝑌 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑠 = 𝑌 → ( toInc ‘ 𝑠 ) = ( toInc ‘ 𝑌 ) )
2	1	eleq1d	⊢ ( 𝑠 = 𝑌 → ( ( toInc ‘ 𝑠 ) ∈ Dirset ↔ ( toInc ‘ 𝑌 ) ∈ Dirset ) )
3		unieq	⊢ ( 𝑠 = 𝑌 → ∪ 𝑠 = ∪ 𝑌 )
4	3	eleq1d	⊢ ( 𝑠 = 𝑌 → ( ∪ 𝑠 ∈ 𝐶 ↔ ∪ 𝑌 ∈ 𝐶 ) )
5	2 4	imbi12d	⊢ ( 𝑠 = 𝑌 → ( ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ↔ ( ( toInc ‘ 𝑌 ) ∈ Dirset → ∪ 𝑌 ∈ 𝐶 ) ) )
6		isacs3lem	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) ) )
7	6	simprd	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
8	7	adantr	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → ∀ 𝑠 ∈ 𝒫 𝐶 ( ( toInc ‘ 𝑠 ) ∈ Dirset → ∪ 𝑠 ∈ 𝐶 ) )
9		elpw2g	⊢ ( 𝐶 ∈ ( ACS ‘ 𝑋 ) → ( 𝑌 ∈ 𝒫 𝐶 ↔ 𝑌 ⊆ 𝐶 ) )
10	9	biimpar	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → 𝑌 ∈ 𝒫 𝐶 )
11	5 8 10	rspcdva	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ) → ( ( toInc ‘ 𝑌 ) ∈ Dirset → ∪ 𝑌 ∈ 𝐶 ) )
12	11	3impia	⊢ ( ( 𝐶 ∈ ( ACS ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝐶 ∧ ( toInc ‘ 𝑌 ) ∈ Dirset ) → ∪ 𝑌 ∈ 𝐶 )