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

Metamath Proof Explorer

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 0fi 
 |-  (/) 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 ) )