Metamath Proof Explorer


Theorem isacs4lem

Description: In a closure system in which directed unions of closed sets are closed, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 acsdrscl.f
 |-  F = ( mrCls ` C )
2 simpll
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> C e. ( Moore ` X ) )
3 elpwi
 |-  ( t e. ~P ~P X -> t C_ ~P X )
4 3 ad2antrl
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> t C_ ~P X )
5 1 mrcuni
 |-  ( ( C e. ( Moore ` X ) /\ t C_ ~P X ) -> ( F ` U. t ) = ( F ` U. ( F " t ) ) )
6 2 4 5 syl2anc
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. t ) = ( F ` U. ( F " t ) ) )
7 1 mrcf
 |-  ( C e. ( Moore ` X ) -> F : ~P X --> C )
8 7 ffnd
 |-  ( C e. ( Moore ` X ) -> F Fn ~P X )
9 8 adantr
 |-  ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> F Fn ~P X )
10 simpll
 |-  ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> C e. ( Moore ` X ) )
11 simprl
 |-  ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> x C_ y )
12 simprr
 |-  ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> y C_ X )
13 10 1 11 12 mrcssd
 |-  ( ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) /\ ( x C_ y /\ y C_ X ) ) -> ( F ` x ) C_ ( F ` y ) )
14 simprr
 |-  ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` t ) e. Dirset )
15 3 ad2antrl
 |-  ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> t C_ ~P X )
16 1 fvexi
 |-  F e. _V
17 16 imaex
 |-  ( F " t ) e. _V
18 17 a1i
 |-  ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F " t ) e. _V )
19 9 13 14 15 18 ipodrsima
 |-  ( ( C e. ( Moore ` X ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` ( F " t ) ) e. Dirset )
20 19 adantlr
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( toInc ` ( F " t ) ) e. Dirset )
21 fveq2
 |-  ( s = ( F " t ) -> ( toInc ` s ) = ( toInc ` ( F " t ) ) )
22 21 eleq1d
 |-  ( s = ( F " t ) -> ( ( toInc ` s ) e. Dirset <-> ( toInc ` ( F " t ) ) e. Dirset ) )
23 unieq
 |-  ( s = ( F " t ) -> U. s = U. ( F " t ) )
24 23 eleq1d
 |-  ( s = ( F " t ) -> ( U. s e. C <-> U. ( F " t ) e. C ) )
25 22 24 imbi12d
 |-  ( s = ( F " t ) -> ( ( ( toInc ` s ) e. Dirset -> U. s e. C ) <-> ( ( toInc ` ( F " t ) ) e. Dirset -> U. ( F " t ) e. C ) ) )
26 simplr
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) )
27 imassrn
 |-  ( F " t ) C_ ran F
28 7 frnd
 |-  ( C e. ( Moore ` X ) -> ran F C_ C )
29 27 28 sstrid
 |-  ( C e. ( Moore ` X ) -> ( F " t ) C_ C )
30 17 elpw
 |-  ( ( F " t ) e. ~P C <-> ( F " t ) C_ C )
31 29 30 sylibr
 |-  ( C e. ( Moore ` X ) -> ( F " t ) e. ~P C )
32 31 ad2antrr
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F " t ) e. ~P C )
33 25 26 32 rspcdva
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( ( toInc ` ( F " t ) ) e. Dirset -> U. ( F " t ) e. C ) )
34 20 33 mpd
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> U. ( F " t ) e. C )
35 1 mrcid
 |-  ( ( C e. ( Moore ` X ) /\ U. ( F " t ) e. C ) -> ( F ` U. ( F " t ) ) = U. ( F " t ) )
36 2 34 35 syl2anc
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. ( F " t ) ) = U. ( F " t ) )
37 6 36 eqtrd
 |-  ( ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) /\ ( t e. ~P ~P X /\ ( toInc ` t ) e. Dirset ) ) -> ( F ` U. t ) = U. ( F " t ) )
38 37 exp32
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> ( t e. ~P ~P X -> ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) )
39 38 ralrimiv
 |-  ( ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) )
40 39 ex
 |-  ( C e. ( Moore ` X ) -> ( A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) )
41 40 imdistani
 |-  ( ( 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 ) ) ) )