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

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