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	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		vpwex	⊢ 𝒫 𝑦 ∈ V
2	1	ax-gen	⊢ ∀ 𝑦 𝒫 𝑦 ∈ V
3		exrecfn	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 𝒫 𝑦 ∈ V ) → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ∈ 𝑥 ) )
4	2 3	mpan2	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ( 𝐴 ⊆ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ∈ 𝑥 ) )