Theorem frrdmss

Description: Show without using the axiom of replacement that the domain of the well-founded recursion generator is a subclass of A . (Contributed by Scott Fenton, 18-Nov-2024)

	Ref	Expression
Hypothesis	frrrel.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
Assertion	frrdmss	$$⊢\mathrm{dom}F\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	$$⊢F=\mathrm{frecs}\left(R,A,G\right)$$
2		eqid	$$⊢\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\}=\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\}$$
3	2 1	frrlem7	$$⊢\mathrm{dom}F\subseteq A$$