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