Metamath Proof Explorer

Theorem isacs3

Description: A closure system is algebraic iff directed unions of closed sets are closed. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion isacs3 
|- ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )

Proof

Step Hyp Ref Expression
1 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
2 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
3 2 isacs4lem 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( ( mrCls ` C ) ` U. t ) = U. ( ( mrCls ` C ) " t ) ) ) )
4 2 isacs4 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( ( mrCls ` C ) ` U. t ) = U. ( ( mrCls ` C ) " t ) ) ) )
5 3 4 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> C e. ( ACS ` X ) )
6 1 5 impbii 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )