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 V K X a 𝒫 X | K a ACS X

Proof

Step Hyp Ref Expression
1 0ss a
2 1 a1bi K a a K a
3 2 rabbii a 𝒫 X | K a = a 𝒫 X | a K a
4 0ss X
5 0fin Fin
6 acsfn X V K X X Fin a 𝒫 X | a K a ACS X
7 4 5 6 mpanr12 X V K X a 𝒫 X | a K a ACS X
8 3 7 eqeltrid X V K X a 𝒫 X | K a ACS X