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 CACSXYCtoIncYDirsetYC

Proof

Step Hyp Ref Expression
1 fveq2 s=YtoIncs=toIncY
2 1 eleq1d s=YtoIncsDirsettoIncYDirset
3 unieq s=Ys=Y
4 3 eleq1d s=YsCYC
5 2 4 imbi12d s=YtoIncsDirsetsCtoIncYDirsetYC
6 isacs3lem CACSXCMooreXs𝒫CtoIncsDirsetsC
7 6 simprd CACSXs𝒫CtoIncsDirsetsC
8 7 adantr CACSXYCs𝒫CtoIncsDirsetsC
9 elpw2g CACSXY𝒫CYC
10 9 biimpar CACSXYCY𝒫C
11 5 8 10 rspcdva CACSXYCtoIncYDirsetYC
12 11 3impia CACSXYCtoIncYDirsetYC