Metamath Proof Explorer


Theorem acsficl2d

Description: In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl . Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsficld.1
|- ( ph -> A e. ( ACS ` X ) )
acsficld.2
|- N = ( mrCls ` A )
acsficld.3
|- ( ph -> S C_ X )
Assertion acsficl2d
|- ( ph -> ( Y e. ( N ` S ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) )

Proof

Step Hyp Ref Expression
1 acsficld.1
 |-  ( ph -> A e. ( ACS ` X ) )
2 acsficld.2
 |-  N = ( mrCls ` A )
3 acsficld.3
 |-  ( ph -> S C_ X )
4 1 2 3 acsficld
 |-  ( ph -> ( N ` S ) = U. ( N " ( ~P S i^i Fin ) ) )
5 4 eleq2d
 |-  ( ph -> ( Y e. ( N ` S ) <-> Y e. U. ( N " ( ~P S i^i Fin ) ) ) )
6 1 acsmred
 |-  ( ph -> A e. ( Moore ` X ) )
7 funmpt
 |-  Fun ( z e. ~P X |-> |^| { w e. A | z C_ w } )
8 2 mrcfval
 |-  ( A e. ( Moore ` X ) -> N = ( z e. ~P X |-> |^| { w e. A | z C_ w } ) )
9 8 funeqd
 |-  ( A e. ( Moore ` X ) -> ( Fun N <-> Fun ( z e. ~P X |-> |^| { w e. A | z C_ w } ) ) )
10 7 9 mpbiri
 |-  ( A e. ( Moore ` X ) -> Fun N )
11 eluniima
 |-  ( Fun N -> ( Y e. U. ( N " ( ~P S i^i Fin ) ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) )
12 6 10 11 3syl
 |-  ( ph -> ( Y e. U. ( N " ( ~P S i^i Fin ) ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) )
13 5 12 bitrd
 |-  ( ph -> ( Y e. ( N ` S ) <-> E. x e. ( ~P S i^i Fin ) Y e. ( N ` x ) ) )