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	⊢ 𝐹 = ( 𝑥 ∈ V ↦ 𝒫 𝑥 )
Assertion	vsetrec	⊢ setrecs ( 𝐹 ) = V

Proof

Step	Hyp	Ref	Expression
1		vsetrec.1	⊢ 𝐹 = ( 𝑥 ∈ V ↦ 𝒫 𝑥 )
2		setind	⊢ ( ∀ 𝑎 ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ setrecs ( 𝐹 ) ) → setrecs ( 𝐹 ) = V )
3		vex	⊢ 𝑎 ∈ V
4	3	pwid	⊢ 𝑎 ∈ 𝒫 𝑎
5		pweq	⊢ ( 𝑥 = 𝑎 → 𝒫 𝑥 = 𝒫 𝑎 )
6	3	pwex	⊢ 𝒫 𝑎 ∈ V
7	5 1 6	fvmpt	⊢ ( 𝑎 ∈ V → ( 𝐹 ‘ 𝑎 ) = 𝒫 𝑎 )
8	3 7	ax-mp	⊢ ( 𝐹 ‘ 𝑎 ) = 𝒫 𝑎
9		eqid	⊢ setrecs ( 𝐹 ) = setrecs ( 𝐹 )
10	3	a1i	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ V )
11		id	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ⊆ setrecs ( 𝐹 ) )
12	9 10 11	setrec1	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → ( 𝐹 ‘ 𝑎 ) ⊆ setrecs ( 𝐹 ) )
13	8 12	eqsstrrid	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝒫 𝑎 ⊆ setrecs ( 𝐹 ) )
14	13	sseld	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → ( 𝑎 ∈ 𝒫 𝑎 → 𝑎 ∈ setrecs ( 𝐹 ) ) )
15	4 14	mpi	⊢ ( 𝑎 ⊆ setrecs ( 𝐹 ) → 𝑎 ∈ setrecs ( 𝐹 ) )
16	2 15	mpg	⊢ setrecs ( 𝐹 ) = V