Theorem acsfn0

Description: Algebraicity of a point closure condition. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	acsfn0	|- ( ( X e. V /\ K e. X ) -> { a e. ~P X | K e. a } e. ( ACS ` X ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ a
2	1	a1bi	|- ( K e. a <-> ( (/) C_ a -> K e. a ) )
3	2	rabbii	|- { a e. ~P X | K e. a } = { a e. ~P X | ( (/) C_ a -> K e. a ) }
4		0ss	|- (/) C_ X
5		0fin	|- (/) e. Fin
6		acsfn	|- ( ( ( X e. V /\ K e. X ) /\ ( (/) C_ X /\ (/) e. Fin ) ) -> { a e. ~P X | ( (/) C_ a -> K e. a ) } e. ( ACS ` X ) )
7	4 5 6	mpanr12	|- ( ( X e. V /\ K e. X ) -> { a e. ~P X | ( (/) C_ a -> K e. a ) } e. ( ACS ` X ) )
8	3 7	eqeltrid	|- ( ( X e. V /\ K e. X ) -> { a e. ~P X | K e. a } e. ( ACS ` X ) )