Theorem acsfn0

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

	Ref	Expression
Assertion	acsfn0	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝑎
2	1	a1bi	⊢ ( 𝐾 ∈ 𝑎 ↔ ( ∅ ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) )
3	2	rabbii	⊢ { 𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎 } = { 𝑎 ∈ 𝒫 𝑋 ∣ ( ∅ ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) }
4		0ss	⊢ ∅ ⊆ 𝑋
5		0fin	⊢ ∅ ∈ Fin
6		acsfn	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) ∧ ( ∅ ⊆ 𝑋 ∧ ∅ ∈ Fin ) ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( ∅ ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
7	4 5 6	mpanr12	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ ( ∅ ⊆ 𝑎 → 𝐾 ∈ 𝑎 ) } ∈ ( ACS ‘ 𝑋 ) )
8	3 7	eqeltrid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝐾 ∈ 𝑋 ) → { 𝑎 ∈ 𝒫 𝑋 ∣ 𝐾 ∈ 𝑎 } ∈ ( ACS ‘ 𝑋 ) )