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 0fi ⊢ ∅ ∈ 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