Metamath Proof Explorer

Theorem isacs5lem

Description: If closure commutes with directed unions, then the closure of a set is the closure of its finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f 
|- F = ( mrCls ` C )
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f 
 |-  F = ( mrCls ` C )
2 unifpw 
 |-  U. ( ~P s i^i Fin ) = s
3 2 fveq2i 
 |-  ( F ` U. ( ~P s i^i Fin ) ) = ( F ` s )
4 vex 
 |-  s e. _V
5 fpwipodrs 
 |-  ( s e. _V -> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset )
6 4 5 mp1i 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset )
7 fveq2 
 |-  ( t = ( ~P s i^i Fin ) -> ( toInc ` t ) = ( toInc ` ( ~P s i^i Fin ) ) )
8 7 eleq1d 
 |-  ( t = ( ~P s i^i Fin ) -> ( ( toInc ` t ) e. Dirset <-> ( toInc ` ( ~P s i^i Fin ) ) e. Dirset ) )
9 unieq 
 |-  ( t = ( ~P s i^i Fin ) -> U. t = U. ( ~P s i^i Fin ) )
10 9 fveq2d 
 |-  ( t = ( ~P s i^i Fin ) -> ( F ` U. t ) = ( F ` U. ( ~P s i^i Fin ) ) )
11 imaeq2 
 |-  ( t = ( ~P s i^i Fin ) -> ( F " t ) = ( F " ( ~P s i^i Fin ) ) )
12 11 unieqd 
 |-  ( t = ( ~P s i^i Fin ) -> U. ( F " t ) = U. ( F " ( ~P s i^i Fin ) ) )
13 10 12 eqeq12d 
 |-  ( t = ( ~P s i^i Fin ) -> ( ( F ` U. t ) = U. ( F " t ) <-> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) )
14 8 13 imbi12d 
 |-  ( t = ( ~P s i^i Fin ) -> ( ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) <-> ( ( toInc ` ( ~P s i^i Fin ) ) e. Dirset -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) ) )
15 simplr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) )
16 inss1 
 |-  ( ~P s i^i Fin ) C_ ~P s
17 elpwi 
 |-  ( s e. ~P X -> s C_ X )
18 17 sspwd 
 |-  ( s e. ~P X -> ~P s C_ ~P X )
19 18 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ~P s C_ ~P X )
20 16 19 sstrid 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) C_ ~P X )
21 vpwex 
 |-  ~P s e. _V
22 21 inex1 
 |-  ( ~P s i^i Fin ) e. _V
23 22 elpw 
 |-  ( ( ~P s i^i Fin ) e. ~P ~P X <-> ( ~P s i^i Fin ) C_ ~P X )
24 20 23 sylibr 
 |-  ( ( C e. ( Moore ` X ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) e. ~P ~P X )
25 24 adantlr 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( ~P s i^i Fin ) e. ~P ~P X )
26 14 15 25 rspcdva 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( ( toInc ` ( ~P s i^i Fin ) ) e. Dirset -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) ) )
27 6 26 mpd 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( F ` U. ( ~P s i^i Fin ) ) = U. ( F " ( ~P s i^i Fin ) ) )
28 3 27 eqtr3id 
 |-  ( ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) /\ s e. ~P X ) -> ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) )
29 28 ralrimiva 
 |-  ( ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) )
30 29 ex 
 |-  ( C e. ( Moore ` X ) -> ( A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
31 30 imdistani 
 |-  ( ( 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 ) ) ) )