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=\mathrm{setrecs}\left(F\right)$$
	setrecsres.2	$$⊢\phi \to \mathrm{Fun}F$$
Assertion	setrecsres	$$⊢\phi \to B=\mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		setrecsres.1	$$⊢B=\mathrm{setrecs}\left(F\right)$$
2		setrecsres.2	$$⊢\phi \to \mathrm{Fun}F$$
3		id	$$⊢x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\to x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
4		resss	$$⊢{F\upharpoonright }_{𝒫B}\subseteq F$$
5	4	a1i	$$⊢\phi \to {F\upharpoonright }_{𝒫B}\subseteq F$$
6	2 5	setrecsss	$$⊢\phi \to \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\subseteq \mathrm{setrecs}\left(F\right)$$
7	6 1	sseqtrrdi	$$⊢\phi \to \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\subseteq B$$
8	3 7	sylan9ssr	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)\to x\subseteq B$$
9		velpw	$$⊢x\in 𝒫B\leftrightarrow x\subseteq B$$
10		fvres	$$⊢x\in 𝒫B\to \left({F\upharpoonright }_{𝒫B}\right)\left(x\right)=F\left(x\right)$$
11	9 10	sylbir	$$⊢x\subseteq B\to \left({F\upharpoonright }_{𝒫B}\right)\left(x\right)=F\left(x\right)$$
12	8 11	syl	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)\to \left({F\upharpoonright }_{𝒫B}\right)\left(x\right)=F\left(x\right)$$
13		eqid	$$⊢\mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)=\mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
14		vex	$$⊢x\in \mathrm{V}$$
15	14	a1i	$$⊢x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\to x\in \mathrm{V}$$
16	13 15 3	setrec1	$$⊢x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\to \left({F\upharpoonright }_{𝒫B}\right)\left(x\right)\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
17	16	adantl	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)\to \left({F\upharpoonright }_{𝒫B}\right)\left(x\right)\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
18	12 17	eqsstrrd	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
19	18	ex	$$⊢\phi \to \left(x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)$$
20	19	alrimiv	$$⊢\phi \to \forall x\left(x\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)\right)$$
21	1 20	setrec2v	$$⊢\phi \to B\subseteq \mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$
22	21 7	eqssd	$$⊢\phi \to B=\mathrm{setrecs}\left(\left({F\upharpoonright }_{𝒫B}\right)\right)$$