Metamath Proof Explorer

Theorem acsdrscl

Description: In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f ⊢ F = mrCls ⁡ C
Assertion acsdrscl ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ 𝒫 X ∧ toInc ⁡ Y ∈ Dirset → F ⁡ ⋃ Y = ⋃ F Y

Proof

Step Hyp Ref Expression
1 acsdrscl.f ⊢ F = mrCls ⁡ C
2 fveq2 ⊢ t = Y → toInc ⁡ t = toInc ⁡ Y
3 2 eleq1d ⊢ t = Y → toInc ⁡ t ∈ Dirset ↔ toInc ⁡ Y ∈ Dirset
4 unieq ⊢ t = Y → ⋃ t = ⋃ Y
5 4 fveq2d ⊢ t = Y → F ⁡ ⋃ t = F ⁡ ⋃ Y
6 imaeq2 ⊢ t = Y → F t = F Y
7 6 unieqd ⊢ t = Y → ⋃ F t = ⋃ F Y
8 5 7 eqeq12d ⊢ t = Y → F ⁡ ⋃ t = ⋃ F t ↔ F ⁡ ⋃ Y = ⋃ F Y
9 3 8 imbi12d ⊢ t = Y → toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t ↔ toInc ⁡ Y ∈ Dirset → F ⁡ ⋃ Y = ⋃ F Y
10 isacs3lem ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C
11 1 isacs4lem ⊢ C ∈ Moore ⁡ X ∧ ∀ s ∈ 𝒫 C toInc ⁡ s ∈ Dirset → ⋃ s ∈ C → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
12 10 11 syl ⊢ C ∈ ACS ⁡ X → C ∈ Moore ⁡ X ∧ ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
13 12 simprd ⊢ C ∈ ACS ⁡ X → ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
14 13 adantr ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ 𝒫 X → ∀ t ∈ 𝒫 𝒫 X toInc ⁡ t ∈ Dirset → F ⁡ ⋃ t = ⋃ F t
15 elfvdm ⊢ C ∈ ACS ⁡ X → X ∈ dom ⁡ ACS
16 pwexg ⊢ X ∈ dom ⁡ ACS → 𝒫 X ∈ V
17 elpw2g ⊢ 𝒫 X ∈ V → Y ∈ 𝒫 𝒫 X ↔ Y ⊆ 𝒫 X
18 15 16 17 3syl ⊢ C ∈ ACS ⁡ X → Y ∈ 𝒫 𝒫 X ↔ Y ⊆ 𝒫 X
19 18 biimpar ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ 𝒫 X → Y ∈ 𝒫 𝒫 X
20 9 14 19 rspcdva ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ 𝒫 X → toInc ⁡ Y ∈ Dirset → F ⁡ ⋃ Y = ⋃ F Y
21 20 3impia ⊢ C ∈ ACS ⁡ X ∧ Y ⊆ 𝒫 X ∧ toInc ⁡ Y ∈ Dirset → F ⁡ ⋃ Y = ⋃ F Y