Theorem setrecsres

Description: A recursively generated class is unaffected when its input function is restricted to subsets of the class. (Contributed by Emmett Weisz, 14-Mar-2022)

	Ref	Expression
Hypotheses	setrecsres.1	|- B = setrecs ( F )
	setrecsres.2	|- ( ph -> Fun F )
Assertion	setrecsres	|- ( ph -> B = setrecs ( ( F |` ~P B ) ) )

Proof

Step	Hyp	Ref	Expression
1		setrecsres.1	|- B = setrecs ( F )
2		setrecsres.2	|- ( ph -> Fun F )
3		id	|- ( x C_ setrecs ( ( F |` ~P B ) ) -> x C_ setrecs ( ( F |` ~P B ) ) )
4		resss	|- ( F |` ~P B ) C_ F
5	4	a1i	|- ( ph -> ( F |` ~P B ) C_ F )
6	2 5	setrecsss	|- ( ph -> setrecs ( ( F |` ~P B ) ) C_ setrecs ( F ) )
7	6 1	sseqtrrdi	|- ( ph -> setrecs ( ( F |` ~P B ) ) C_ B )
8	3 7	sylan9ssr	|- ( ( ph /\ x C_ setrecs ( ( F |` ~P B ) ) ) -> x C_ B )
9		velpw	|- ( x e. ~P B <-> x C_ B )
10		fvres	|- ( x e. ~P B -> ( ( F |` ~P B ) ` x ) = ( F ` x ) )
11	9 10	sylbir	|- ( x C_ B -> ( ( F |` ~P B ) ` x ) = ( F ` x ) )
12	8 11	syl	|- ( ( ph /\ x C_ setrecs ( ( F |` ~P B ) ) ) -> ( ( F |` ~P B ) ` x ) = ( F ` x ) )
13		eqid	|- setrecs ( ( F |` ~P B ) ) = setrecs ( ( F |` ~P B ) )
14		vex	|- x e. _V
15	14	a1i	|- ( x C_ setrecs ( ( F |` ~P B ) ) -> x e. _V )
16	13 15 3	setrec1	|- ( x C_ setrecs ( ( F |` ~P B ) ) -> ( ( F |` ~P B ) ` x ) C_ setrecs ( ( F |` ~P B ) ) )
17	16	adantl	|- ( ( ph /\ x C_ setrecs ( ( F |` ~P B ) ) ) -> ( ( F |` ~P B ) ` x ) C_ setrecs ( ( F |` ~P B ) ) )
18	12 17	eqsstrrd	|- ( ( ph /\ x C_ setrecs ( ( F |` ~P B ) ) ) -> ( F ` x ) C_ setrecs ( ( F |` ~P B ) ) )
19	18	ex	|- ( ph -> ( x C_ setrecs ( ( F |` ~P B ) ) -> ( F ` x ) C_ setrecs ( ( F |` ~P B ) ) ) )
20	19	alrimiv	|- ( ph -> A. x ( x C_ setrecs ( ( F |` ~P B ) ) -> ( F ` x ) C_ setrecs ( ( F |` ~P B ) ) ) )
21	1 20	setrec2v	|- ( ph -> B C_ setrecs ( ( F |` ~P B ) ) )
22	21 7	eqssd	|- ( ph -> B = setrecs ( ( F |` ~P B ) ) )