Metamath Proof Explorer

Theorem isacs5

Description: A closure system is algebraic iff the closure of a generating set is the union of the closures of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 acsdrscl.f 
 |-  F = ( mrCls ` C )
2 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
3 1 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 -> ( F ` U. t ) = U. ( F " t ) ) ) )
4 1 isacs5lem 
 |-  ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
5 2 3 4 3syl 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
6 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> C e. ( Moore ` X ) )
7 elpwi 
 |-  ( s e. ~P X -> s C_ X )
8 1 mrcidb2 
 |-  ( ( C e. ( Moore ` X ) /\ s C_ X ) -> ( s e. C <-> ( F ` s ) C_ s ) )
9 7 8 sylan2 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( s e. C <-> ( F ` s ) C_ s ) )
10 9 adantr 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( s e. C <-> ( F ` s ) C_ s ) )
11 simpr 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) )
12 1 mrcf 
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
13 ffun 
 |-  ( F : ~P X --> C -> Fun F )
14 funiunfv 
 |-  ( Fun F -> U_ t e. ( ~P s i^i Fin ) ( F ` t ) = U. ( F " ( ~P s i^i Fin ) ) )
15 12 13 14 3syl 
 |-  ( C e. ( Moore ` X ) -> U_ t e. ( ~P s i^i Fin ) ( F ` t ) = U. ( F " ( ~P s i^i Fin ) ) )
16 15 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> U_ t e. ( ~P s i^i Fin ) ( F ` t ) = U. ( F " ( ~P s i^i Fin ) ) )
17 11 16 eqtr4d 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( F ` s ) = U_ t e. ( ~P s i^i Fin ) ( F ` t ) )
18 17 sseq1d 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( ( F ` s ) C_ s <-> U_ t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) )
19 iunss 
 |-  ( U_ t e. ( ~P s i^i Fin ) ( F ` t ) C_ s <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s )
20 18 19 bitrdi 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( ( F ` s ) C_ s <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) )
21 10 20 bitrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ s e. ~P X ) /\ ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> ( s e. C <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) )
22 21 ex 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) -> ( s e. C <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) ) )
23 22 ralimdva 
 |-  ( C e. ( Moore ` X ) -> ( A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) -> A. s e. ~P X ( s e. C <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) ) )
24 23 imp 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> A. s e. ~P X ( s e. C <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) )
25 1 isacs2 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. t e. ( ~P s i^i Fin ) ( F ` t ) C_ s ) ) )
26 6 24 25 sylanbrc 
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) -> C e. ( ACS ` X ) )
27 5 26 impbii 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )