Metamath Proof Explorer

Theorem isacs4

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

Ref Expression
Hypothesis acsdrscl.f 
|- F = ( mrCls ` C )
Assertion isacs4 
|- ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f 
 |-  F = ( mrCls ` C )
2 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. t e. ~P C ( ( toInc ` t ) e. Dirset -> U. t e. C ) ) )
3 1 isacs4lem 
 |-  ( ( C e. ( Moore ` X ) /\ A. t e. ~P C ( ( toInc ` t ) e. Dirset -> U. t e. C ) ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) )
4 2 3 syl 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) )
5 1 isacs5lem 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) -> ( C e. ( Moore ` X ) /\ A. t e. ~P X ( F ` t ) = U. ( F " ( ~P t i^i Fin ) ) ) )
6 1 isacs5 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. t e. ~P X ( F ` t ) = U. ( F " ( ~P t i^i Fin ) ) ) )
7 5 6 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) -> C e. ( ACS ` X ) )
8 4 7 impbii 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P ~P X ( ( toInc ` s ) e. Dirset -> ( F ` U. s ) = U. ( F " s ) ) ) )