acsfn0

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

		Ref	Expression
	Assertion	acsfn0	$⊢ (X \in V \land K \in X) \to \{a \in 𝒫 X \| K \in a\} \in ACS (X)$

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq a$
2	1	a1bi	$⊢ K \in a \leftrightarrow (\emptyset \subseteq a \to K \in a)$
3	2	rabbii	$⊢ \{a \in 𝒫 X \| K \in a\} = \{a \in 𝒫 X \| (\emptyset \subseteq a \to K \in a)\}$
4		0ss	$⊢ \emptyset \subseteq X$
5		0fi	$⊢ \emptyset \in Fin$
6		acsfn	$⊢ ((X \in V \land K \in X) \land (\emptyset \subseteq X \land \emptyset \in Fin)) \to \{a \in 𝒫 X \| (\emptyset \subseteq a \to K \in a)\} \in ACS (X)$
7	4 5 6	mpanr12	$⊢ (X \in V \land K \in X) \to \{a \in 𝒫 X \| (\emptyset \subseteq a \to K \in a)\} \in ACS (X)$
8	3 7	eqeltrid	$⊢ (X \in V \land K \in X) \to \{a \in 𝒫 X \| K \in a\} \in ACS (X)$

Metamath Proof Explorer