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=⋃FY

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→Ft=FY
7 6 unieqd ⊢t=Y→⋃Ft=⋃FY
8 5 7 eqeq12d ⊢t=Y→F⁡⋃t=⋃Ft↔F⁡⋃Y=⋃FY
9 3 8 imbi12d ⊢t=Y→toInc⁡t∈Dirset→F⁡⋃t=⋃Ft↔toInc⁡Y∈Dirset→F⁡⋃Y=⋃FY
10 isacs3lem ⊢C∈ACS⁡X→C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C
11 1 isacs4lem ⊢C∈Moore⁡X∧∀s∈𝒫CtoInc⁡s∈Dirset→⋃s∈C→C∈Moore⁡X∧∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft
12 10 11 syl ⊢C∈ACS⁡X→C∈Moore⁡X∧∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft
13 12 simprd ⊢C∈ACS⁡X→∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft
14 13 adantr ⊢C∈ACS⁡X∧Y⊆𝒫X→∀t∈𝒫𝒫XtoInc⁡t∈Dirset→F⁡⋃t=⋃Ft
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=⋃FY
21 20 3impia ⊢C∈ACS⁡X∧Y⊆𝒫X∧toInc⁡Y∈Dirset→F⁡⋃Y=⋃FY