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 e. ( ACS ` X ) /\ Y C_ C /\ ( toInc ` Y ) e. Dirset ) -> U. Y e. C )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( s = Y -> ( toInc ` s ) = ( toInc ` Y ) )
2 1 eleq1d 
 |-  ( s = Y -> ( ( toInc ` s ) e. Dirset <-> ( toInc ` Y ) e. Dirset ) )
3 unieq 
 |-  ( s = Y -> U. s = U. Y )
4 3 eleq1d 
 |-  ( s = Y -> ( U. s e. C <-> U. Y e. C ) )
5 2 4 imbi12d 
 |-  ( s = Y -> ( ( ( toInc ` s ) e. Dirset -> U. s e. C ) <-> ( ( toInc ` Y ) e. Dirset -> U. Y e. C ) ) )
6 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
7 6 simprd 
 |-  ( C e. ( ACS ` X ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
8 7 adantr 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ C ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
9 elpw2g 
 |-  ( C e. ( ACS ` X ) -> ( Y e. ~P C <-> Y C_ C ) )
10 9 biimpar 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ C ) -> Y e. ~P C )
11 5 8 10 rspcdva 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ C ) -> ( ( toInc ` Y ) e. Dirset -> U. Y e. C ) )
12 11 3impia 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ C /\ ( toInc ` Y ) e. Dirset ) -> U. Y e. C )