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 ) ) ) )