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	$$⊢\phi \to \mathrm{Fun}G$$
	setrecsss.2	$$⊢\phi \to F\subseteq G$$
Assertion	setrecsss	$$⊢\phi \to \mathrm{setrecs}\left(F\right)\subseteq \mathrm{setrecs}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		setrecsss.1	$$⊢\phi \to \mathrm{Fun}G$$
2		setrecsss.2	$$⊢\phi \to F\subseteq G$$
3		eqid	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{setrecs}\left(F\right)$$
4		imass1	$$⊢F\subseteq G\to F\left[\left\{x\right\}\right]\subseteq G\left[\left\{x\right\}\right]$$
5	2 4	syl	$$⊢\phi \to F\left[\left\{x\right\}\right]\subseteq G\left[\left\{x\right\}\right]$$
6	5	unissd	$$⊢\phi \to \bigcup F\left[\left\{x\right\}\right]\subseteq \bigcup G\left[\left\{x\right\}\right]$$
7		funss	$$⊢F\subseteq G\to \left(\mathrm{Fun}G\to \mathrm{Fun}F\right)$$
8	2 1 7	sylc	$$⊢\phi \to \mathrm{Fun}F$$
9		funfv	$$⊢\mathrm{Fun}F\to F\left(x\right)=\bigcup F\left[\left\{x\right\}\right]$$
10	8 9	syl	$$⊢\phi \to F\left(x\right)=\bigcup F\left[\left\{x\right\}\right]$$
11		funfv	$$⊢\mathrm{Fun}G\to G\left(x\right)=\bigcup G\left[\left\{x\right\}\right]$$
12	1 11	syl	$$⊢\phi \to G\left(x\right)=\bigcup G\left[\left\{x\right\}\right]$$
13	6 10 12	3sstr4d	$$⊢\phi \to F\left(x\right)\subseteq G\left(x\right)$$
14	13	adantr	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(G\right)\right)\to F\left(x\right)\subseteq G\left(x\right)$$
15		eqid	$$⊢\mathrm{setrecs}\left(G\right)=\mathrm{setrecs}\left(G\right)$$
16		vex	$$⊢x\in \mathrm{V}$$
17	16	a1i	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(G\right)\right)\to x\in \mathrm{V}$$
18		simpr	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(G\right)\right)\to x\subseteq \mathrm{setrecs}\left(G\right)$$
19	15 17 18	setrec1	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(G\right)\right)\to G\left(x\right)\subseteq \mathrm{setrecs}\left(G\right)$$
20	14 19	sstrd	$$⊢\left(\phi \wedge x\subseteq \mathrm{setrecs}\left(G\right)\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(G\right)$$
21	20	ex	$$⊢\phi \to \left(x\subseteq \mathrm{setrecs}\left(G\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(G\right)\right)$$
22	21	alrimiv	$$⊢\phi \to \forall x\left(x\subseteq \mathrm{setrecs}\left(G\right)\to F\left(x\right)\subseteq \mathrm{setrecs}\left(G\right)\right)$$
23	3 22	setrec2v	$$⊢\phi \to \mathrm{setrecs}\left(F\right)\subseteq \mathrm{setrecs}\left(G\right)$$