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