Theorem setrecsss

Description: The setrecs operator respects the subset relation between two functions F and G . (Contributed by Emmett Weisz, 13-Mar-2022)

	Ref	Expression
Hypotheses	setrecsss.1	⊢ ( 𝜑 → Fun 𝐺 )
	setrecsss.2	⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
Assertion	setrecsss	⊢ ( 𝜑 → setrecs ( 𝐹 ) ⊆ setrecs ( 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		setrecsss.1	⊢ ( 𝜑 → Fun 𝐺 )
2		setrecsss.2	⊢ ( 𝜑 → 𝐹 ⊆ 𝐺 )
3		eqid	⊢ setrecs ( 𝐹 ) = setrecs ( 𝐹 )
4		imass1	⊢ ( 𝐹 ⊆ 𝐺 → ( 𝐹 “ { 𝑥 } ) ⊆ ( 𝐺 “ { 𝑥 } ) )
5	2 4	syl	⊢ ( 𝜑 → ( 𝐹 “ { 𝑥 } ) ⊆ ( 𝐺 “ { 𝑥 } ) )
6	5	unissd	⊢ ( 𝜑 → ∪ ( 𝐹 “ { 𝑥 } ) ⊆ ∪ ( 𝐺 “ { 𝑥 } ) )
7		funss	⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐺 → Fun 𝐹 ) )
8	2 1 7	sylc	⊢ ( 𝜑 → Fun 𝐹 )
9		funfv	⊢ ( Fun 𝐹 → ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ { 𝑥 } ) )
10	8 9	syl	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑥 ) = ∪ ( 𝐹 “ { 𝑥 } ) )
11		funfv	⊢ ( Fun 𝐺 → ( 𝐺 ‘ 𝑥 ) = ∪ ( 𝐺 “ { 𝑥 } ) )
12	1 11	syl	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑥 ) = ∪ ( 𝐺 “ { 𝑥 } ) )
13	6 10 12	3sstr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ 𝑥 ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐺 ‘ 𝑥 ) )
15		eqid	⊢ setrecs ( 𝐺 ) = setrecs ( 𝐺 )
16		vex	⊢ 𝑥 ∈ V
17	16	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( 𝐺 ) ) → 𝑥 ∈ V )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( 𝐺 ) ) → 𝑥 ⊆ setrecs ( 𝐺 ) )
19	15 17 18	setrec1	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ⊆ setrecs ( 𝐺 ) )
20	14 19	sstrd	⊢ ( ( 𝜑 ∧ 𝑥 ⊆ setrecs ( 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( 𝐺 ) )
21	20	ex	⊢ ( 𝜑 → ( 𝑥 ⊆ setrecs ( 𝐺 ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( 𝐺 ) ) )
22	21	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ⊆ setrecs ( 𝐺 ) → ( 𝐹 ‘ 𝑥 ) ⊆ setrecs ( 𝐺 ) ) )
23	3 22	setrec2v	⊢ ( 𝜑 → setrecs ( 𝐹 ) ⊆ setrecs ( 𝐺 ) )