Theorem 0setrec

Description: If a function sends the empty set to itself, the function will not recursively generate any sets, regardless of its other values. (Contributed by Emmett Weisz, 23-Jun-2021)

	Ref	Expression
Hypothesis	0setrec.1	$$⊢\phi \to F\left(\varnothing \right)=\varnothing$$
Assertion	0setrec	$$⊢\phi \to \mathrm{setrecs}\left(F\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0setrec.1	$$⊢\phi \to F\left(\varnothing \right)=\varnothing$$
2		eqid	$$⊢\mathrm{setrecs}\left(F\right)=\mathrm{setrecs}\left(F\right)$$
3		ss0	$$⊢x\subseteq \varnothing \to x=\varnothing$$
4		fveq2	$$⊢x=\varnothing \to F\left(x\right)=F\left(\varnothing \right)$$
5	4 1	sylan9eqr	$$⊢\left(\phi \wedge x=\varnothing \right)\to F\left(x\right)=\varnothing$$
6	5	ex	$$⊢\phi \to \left(x=\varnothing \to F\left(x\right)=\varnothing \right)$$
7		eqimss	$$⊢F\left(x\right)=\varnothing \to F\left(x\right)\subseteq \varnothing$$
8	3 6 7	syl56	$$⊢\phi \to \left(x\subseteq \varnothing \to F\left(x\right)\subseteq \varnothing \right)$$
9	8	alrimiv	$$⊢\phi \to \forall x\left(x\subseteq \varnothing \to F\left(x\right)\subseteq \varnothing \right)$$
10	2 9	setrec2v	$$⊢\phi \to \mathrm{setrecs}\left(F\right)\subseteq \varnothing$$
11		ss0	$$⊢\mathrm{setrecs}\left(F\right)\subseteq \varnothing \to \mathrm{setrecs}\left(F\right)=\varnothing$$
12	10 11	syl	$$⊢\phi \to \mathrm{setrecs}\left(F\right)=\varnothing$$