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