Theorem frrlem7

Description: Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of A . (Contributed by Scott Fenton, 27-Aug-2022)

	Ref	Expression
Hypotheses	frrlem5.1	$$⊢B=\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
	frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frrlem7	$$⊢\mathrm{dom}F\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		frrlem5.1	$$⊢B=\left\{f|\exists x\left(fFnx\wedge \left(x\subseteq A\wedge \forall y\in xPred\left(R,A,y\right)\subseteq x\right)\wedge \forall y\in xf\left(y\right)=yG\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
2		frrlem5.2	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
3	1 2	frrlem5	$$⊢F=\bigcup B$$
4	3	dmeqi	$$⊢\mathrm{dom}F=\mathrm{dom}\bigcup B$$
5		dmuni	$$⊢\mathrm{dom}\bigcup B=\bigcup _{g\in B}\mathrm{dom}g$$
6	4 5	eqtri	$$⊢\mathrm{dom}F=\bigcup _{g\in B}\mathrm{dom}g$$
7	6	sseq1i	$$⊢\mathrm{dom}F\subseteq A\leftrightarrow \bigcup _{g\in B}\mathrm{dom}g\subseteq A$$
8		iunss	$$⊢\bigcup _{g\in B}\mathrm{dom}g\subseteq A\leftrightarrow \forall g\in B\mathrm{dom}g\subseteq A$$
9	7 8	bitri	$$⊢\mathrm{dom}F\subseteq A\leftrightarrow \forall g\in B\mathrm{dom}g\subseteq A$$
10	1	frrlem3	$$⊢g\in B\to \mathrm{dom}g\subseteq A$$
11	9 10	mprgbir	$$⊢\mathrm{dom}F\subseteq A$$