Metamath Proof Explorer

Theorem acsdrscl

Description: In an algebraic closure system, closure commutes with directed unions. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f 
|- F = ( mrCls ` C )
Assertion acsdrscl 
|- ( ( C e. ( ACS ` X ) /\ Y C_ ~P X /\ ( toInc ` Y ) e. Dirset ) -> ( F ` U. Y ) = U. ( F " Y ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f 
 |-  F = ( mrCls ` C )
2 fveq2 
 |-  ( t = Y -> ( toInc ` t ) = ( toInc ` Y ) )
3 2 eleq1d 
 |-  ( t = Y -> ( ( toInc ` t ) e. Dirset <-> ( toInc ` Y ) e. Dirset ) )
4 unieq 
 |-  ( t = Y -> U. t = U. Y )
5 4 fveq2d 
 |-  ( t = Y -> ( F ` U. t ) = ( F ` U. Y ) )
6 imaeq2 
 |-  ( t = Y -> ( F " t ) = ( F " Y ) )
7 6 unieqd 
 |-  ( t = Y -> U. ( F " t ) = U. ( F " Y ) )
8 5 7 eqeq12d 
 |-  ( t = Y -> ( ( F ` U. t ) = U. ( F " t ) <-> ( F ` U. Y ) = U. ( F " Y ) ) )
9 3 8 imbi12d 
 |-  ( t = Y -> ( ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) <-> ( ( toInc ` Y ) e. Dirset -> ( F ` U. Y ) = U. ( F " Y ) ) ) )
10 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
11 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 ) ) ) )
12 10 11 syl 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) ) )
13 12 simprd 
 |-  ( C e. ( ACS ` X ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) )
14 13 adantr 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ ~P X ) -> A. t e. ~P ~P X ( ( toInc ` t ) e. Dirset -> ( F ` U. t ) = U. ( F " t ) ) )
15 elfvdm 
 |-  ( C e. ( ACS ` X ) -> X e. dom ACS )
16 pwexg 
 |-  ( X e. dom ACS -> ~P X e. _V )
17 elpw2g 
 |-  ( ~P X e. _V -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
18 15 16 17 3syl 
 |-  ( C e. ( ACS ` X ) -> ( Y e. ~P ~P X <-> Y C_ ~P X ) )
19 18 biimpar 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ ~P X ) -> Y e. ~P ~P X )
20 9 14 19 rspcdva 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ ~P X ) -> ( ( toInc ` Y ) e. Dirset -> ( F ` U. Y ) = U. ( F " Y ) ) )
21 20 3impia 
 |-  ( ( C e. ( ACS ` X ) /\ Y C_ ~P X /\ ( toInc ` Y ) e. Dirset ) -> ( F ` U. Y ) = U. ( F " Y ) )