Description: An algebraic closure system contains all directed unions of closed sets. (Contributed by Stefan O'Rear, 2-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | acsdrsel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |
|
2 | 1 | eleq1d | |
3 | unieq | |
|
4 | 3 | eleq1d | |
5 | 2 4 | imbi12d | |
6 | isacs3lem | |
|
7 | 6 | simprd | |
8 | 7 | adantr | |
9 | elpw2g | |
|
10 | 9 | biimpar | |
11 | 5 8 10 | rspcdva | |
12 | 11 | 3impia | |