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	⊢ 𝐵 = setrecs ( 𝐹 )
	setrecsres.2	⊢ ( 𝜑 → Fun 𝐹 )
Assertion	setrecsres	⊢ ( 𝜑 → 𝐵 = setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		setrecsres.1	⊢ 𝐵 = setrecs ( 𝐹 )
2		setrecsres.2	⊢ ( 𝜑 → Fun 𝐹 )
3		id	⊢ ( 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) → 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )
4		resss	⊢ ( 𝐹 ↾ 𝒫 𝐵 ) ⊆ 𝐹
5	4	a1i	⊢ ( 𝜑 → ( 𝐹 ↾ 𝒫 𝐵 ) ⊆ 𝐹 )
6	2 5	setrecsss	⊢ ( 𝜑 → setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ⊆ setrecs ( 𝐹 ) )
7	6 1	sseqtrrdi	⊢ ( 𝜑 → setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ⊆ 𝐵 )
8	3 7	sylan9ssr	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) → 𝑥 ⊆ 𝐵 )
9		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵 )
10		fvres	⊢ ( 𝑥 ∈ 𝒫 𝐵 → ( ( 𝐹 ↾ 𝒫 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
11	9 10	sylbir	⊢ ( 𝑥 ⊆ 𝐵 → ( ( 𝐹 ↾ 𝒫 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
12	8 11	syl	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝒫 𝐵 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
13		eqid	⊢ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) = setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) )
14		vex	⊢ 𝑥 ∈ V
15	14	a1i	⊢ ( 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) → 𝑥 ∈ V )
16	13 15 3	setrec1	⊢ ( 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) → ( ( 𝐹 ↾ 𝒫 𝐵 ) ‘ 𝑥 ) ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝒫 𝐵 ) ‘ 𝑥 ) ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )
18	12 17	eqsstrrd	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )
19	18	ex	⊢ ( 𝜑 → ( 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) )
20	19	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) ) )
21	1 20	setrec2v	⊢ ( 𝜑 → 𝐵 ⊆ setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )
22	21 7	eqssd	⊢ ( 𝜑 → 𝐵 = setrecs ( ( 𝐹 ↾ 𝒫 𝐵 ) ) )