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