Metamath Proof Explorer

Theorem acsfiel

Description: A set is closed in an algebraic closure system iff it contains all closures of finite subsets. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Hypothesis isacs2.f 
|- F = ( mrCls ` C )
Assertion acsfiel 
|- ( C e. ( ACS ` X ) -> ( S e. C <-> ( S C_ X /\ A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) )

Proof

Step Hyp Ref Expression
1 isacs2.f 
 |-  F = ( mrCls ` C )
2 acsmre 
 |-  ( C e. ( ACS ` X ) -> C e. ( Moore ` X ) )
3 mress 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> S C_ X )
4 2 3 sylan 
 |-  ( ( C e. ( ACS ` X ) /\ S e. C ) -> S C_ X )
5 4 ex 
 |-  ( C e. ( ACS ` X ) -> ( S e. C -> S C_ X ) )
6 5 pm4.71rd 
 |-  ( C e. ( ACS ` X ) -> ( S e. C <-> ( S C_ X /\ S e. C ) ) )
7 eleq1 
 |-  ( s = S -> ( s e. C <-> S e. C ) )
8 pweq 
 |-  ( s = S -> ~P s = ~P S )
9 8 ineq1d 
 |-  ( s = S -> ( ~P s i^i Fin ) = ( ~P S i^i Fin ) )
10 sseq2 
 |-  ( s = S -> ( ( F ` y ) C_ s <-> ( F ` y ) C_ S ) )
11 9 10 raleqbidv 
 |-  ( s = S -> ( A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) )
12 7 11 bibi12d 
 |-  ( s = S -> ( ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) <-> ( S e. C <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) )
13 1 isacs2 
 |-  ( C e. ( ACS ` X ) <-> ( C e. ( Moore ` X ) /\ A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) ) )
14 13 simprbi 
 |-  ( C e. ( ACS ` X ) -> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
15 14 adantr 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> A. s e. ~P X ( s e. C <-> A. y e. ( ~P s i^i Fin ) ( F ` y ) C_ s ) )
16 elfvdm 
 |-  ( C e. ( ACS ` X ) -> X e. dom ACS )
17 elpw2g 
 |-  ( X e. dom ACS -> ( S e. ~P X <-> S C_ X ) )
18 16 17 syl 
 |-  ( C e. ( ACS ` X ) -> ( S e. ~P X <-> S C_ X ) )
19 18 biimpar 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> S e. ~P X )
20 12 15 19 rspcdva 
 |-  ( ( C e. ( ACS ` X ) /\ S C_ X ) -> ( S e. C <-> A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) )
21 20 pm5.32da 
 |-  ( C e. ( ACS ` X ) -> ( ( S C_ X /\ S e. C ) <-> ( S C_ X /\ A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) )
22 6 21 bitrd 
 |-  ( C e. ( ACS ` X ) -> ( S e. C <-> ( S C_ X /\ A. y e. ( ~P S i^i Fin ) ( F ` y ) C_ S ) ) )