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 = ( x e. _V |-> ~P x )
Assertion	vsetrec	|- setrecs ( F ) = _V

Proof

Step	Hyp	Ref	Expression
1		vsetrec.1	|- F = ( x e. _V |-> ~P x )
2		setind	|- ( A. a ( a C_ setrecs ( F ) -> a e. setrecs ( F ) ) -> setrecs ( F ) = _V )
3		vex	|- a e. _V
4	3	pwid	|- a e. ~P a
5		pweq	|- ( x = a -> ~P x = ~P a )
6		vpwex	|- ~P a e. _V
7	5 1 6	fvmpt	|- ( a e. _V -> ( F ` a ) = ~P a )
8	3 7	ax-mp	|- ( F ` a ) = ~P a
9		eqid	|- setrecs ( F ) = setrecs ( F )
10	3	a1i	|- ( a C_ setrecs ( F ) -> a e. _V )
11		id	|- ( a C_ setrecs ( F ) -> a C_ setrecs ( F ) )
12	9 10 11	setrec1	|- ( a C_ setrecs ( F ) -> ( F ` a ) C_ setrecs ( F ) )
13	8 12	eqsstrrid	|- ( a C_ setrecs ( F ) -> ~P a C_ setrecs ( F ) )
14	13	sseld	|- ( a C_ setrecs ( F ) -> ( a e. ~P a -> a e. setrecs ( F ) ) )
15	4 14	mpi	|- ( a C_ setrecs ( F ) -> a e. setrecs ( F ) )
16	2 15	mpg	|- setrecs ( F ) = _V