Theorem exrecfnpw

Description: For any base set, a set which contains the powerset of all of its own elements exists. (Contributed by ML, 30-Mar-2022)

	Ref	Expression
Assertion	exrecfnpw	$$⊢A\in V\to \exists x\left(A\subseteq x\wedge \forall y\in x𝒫y\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		vpwex	$$⊢𝒫y\in \mathrm{V}$$
2	1	ax-gen	$$⊢\forall y𝒫y\in \mathrm{V}$$
3		exrecfn	$$⊢\left(A\in V\wedge \forall y𝒫y\in \mathrm{V}\right)\to \exists x\left(A\subseteq x\wedge \forall y\in x𝒫y\in x\right)$$
4	2 3	mpan2	$$⊢A\in V\to \exists x\left(A\subseteq x\wedge \forall y\in x𝒫y\in x\right)$$