Theorem vsetrec

Description: Construct _V using set recursion. The proof indirectly uses trcl , which relies on rec , but theoretically C in trcl could be constructed using setrecs instead. The proof of this theorem uses the dummy variable a rather than x to avoid a distinct variable requirement between F and x . (Contributed by Emmett Weisz, 23-Jun-2021)

	Ref	Expression
Hypothesis	vsetrec.1	$$⊢F=\left(x\in \mathrm{V}⟼𝒫x\right)$$
Assertion	vsetrec	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		vsetrec.1	$$⊢F=\left(x\in \mathrm{V}⟼𝒫x\right)$$
2		setind	$$⊢\forall a\left(a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{setrecs}\left(F\right)\right)\to \mathrm{setrecs}\left(F\right)=\mathrm{V}$$
3		vex	$$⊢a\in \mathrm{V}$$
4	3	pwid	$$⊢a\in 𝒫a$$
5		pweq	$$⊢x=a\to 𝒫x=𝒫a$$
6		vpwex	$$⊢𝒫a\in \mathrm{V}$$
7	5 1 6	fvmpt	$$⊢a\in \mathrm{V}\to F\left(a\right)=𝒫a$$
8	3 7	ax-mp	$$⊢F\left(a\right)=𝒫a$$
9		eqid	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{setrecs}\left(F\right)$$
10	3	a1i	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{V}$$
11		id	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to a\subseteq \mathrm{setrecs}\left(F\right)$$
12	9 10 11	setrec1	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to F\left(a\right)\subseteq \mathrm{setrecs}\left(F\right)$$
13	8 12	eqsstrrid	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to 𝒫a\subseteq \mathrm{setrecs}\left(F\right)$$
14	13	sseld	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to \left(a\in 𝒫a\to a\in \mathrm{setrecs}\left(F\right)\right)$$
15	4 14	mpi	$$⊢a\subseteq \mathrm{setrecs}\left(F\right)\to a\in \mathrm{setrecs}\left(F\right)$$
16	2 15	mpg	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{V}$$