Metamath Proof Explorer

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 ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ C ∧ toInc ⁡ Y ∈ Dirset → ⋃ Y ∈ C

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ s = Y → toInc ⁡ s = toInc ⁡ Y
2 1 eleq1d ⊢ s = Y → toInc ⁡ s ∈ Dirset ↔ toInc ⁡ Y ∈ Dirset
3 unieq ⊢ s = Y → ⋃ s = ⋃ Y
4 3 eleq1d ⊢ s = Y → ⋃ s ∈ C ↔ ⋃ Y ∈ C
5 2 4 imbi12d ⊢ s = Y → toInc ⁡ s ∈ Dirset → ⋃ s ∈ C ↔ toInc ⁡ Y ∈ Dirset → ⋃ Y ∈ C
6 isacs3lem ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
7 6 simprd ⊢ C ∈ ACS ⁡ X → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
8 7 adantr ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ C → ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
9 elpw2g ⊢ C ∈ ACS ⁡ X → Y ∈ 𝒫 C ↔ Y ⊆ C
10 9 biimpar ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ C → Y ∈ 𝒫 C
11 5 8 10 rspcdva ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ C → toInc ⁡ Y ∈ Dirset → ⋃ Y ∈ C
12 11 3impia ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ C ∧ toInc ⁡ Y ∈ Dirset → ⋃ Y ∈ C