This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acsficl

Description: A closure in an algebraic closure system is the union of the closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis acsdrscl.f 
|- F = ( mrCls ` C )
Assertion acsficl 
|- ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) )

Proof

Step Hyp Ref Expression
1 acsdrscl.f 
 |-  F = ( mrCls ` C )
2 fveq2 
 |-  ( s = S -> ( F ` s ) = ( F ` S ) )
3 pweq 
 |-  ( s = S -> ~P s = ~P S )
4 3 ineq1d 
 |-  ( s = S -> ( ~P s i^i Fin ) = ( ~P S i^i Fin ) )
5 4 imaeq2d 
 |-  ( s = S -> ( F " ( ~P s i^i Fin ) ) = ( F " ( ~P S i^i Fin ) ) )
6 5 unieqd 
 |-  ( s = S -> U. ( F " ( ~P s i^i Fin ) ) = U. ( F " ( ~P S i^i Fin ) ) )
7 2 6 eqeq12d 
 |-  ( s = S -> ( ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) <-> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) ) )
8 isacs3lem 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P C ( ( toInc ` s ) e. Dirset -> U. s e. C ) ) )
9 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 ) ) ) )
10 1 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 ) ) ) )
11 8 9 10 3syl 
 |-  ( C e. ( ACS ` X ) -> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) ) )
12 11 simprd 
 |-  ( C e. ( ACS ` X ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) )
13 12 adantr 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> A. s e. ~P X ( F ` s ) = U. ( F " ( ~P s i^i Fin ) ) )
14 elfvdm 
 |-  ( C e. ( ACS ` X ) -> X e. dom ACS )
15 elpw2g 
 |-  ( X e. dom ACS -> ( S e. ~P X <-> S C_ X ) )
16 14 15 syl 
 |-  ( C e. ( ACS ` X ) -> ( S e. ~P X <-> S C_ X ) )
17 16 biimpar 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> S e. ~P X )
18 7 13 17 rspcdva 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( F ` S ) = U. ( F " ( ~P S i^i Fin ) ) )