Theorem wfrdmss

Description: The domain of the well-ordered recursion generator is a subclass of A . (Contributed by Scott Fenton, 21-Apr-2011)

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

Proof

Step	Hyp	Ref	Expression
1		wfrlem6.1	$$⊢F=\mathrm{wrecs}\left(R,A,G\right)$$
2		df-wrecs	$$⊢\mathrm{wrecs}\left(R,A,G\right)=\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
3	1 2	eqtri	$$⊢F=\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
4	3	dmeqi	$$⊢\mathrm{dom}F=\mathrm{dom}\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
5		dmuni	$$⊢\mathrm{dom}\bigcup \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}=\bigcup _{g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}}\mathrm{dom}g$$
6	4 5	eqtri	$$⊢\mathrm{dom}F=\bigcup _{g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}}\mathrm{dom}g$$
7		iunss	$$⊢\bigcup _{g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}}\mathrm{dom}g\subseteq A\leftrightarrow \forall g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\mathrm{dom}g\subseteq A$$
8		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)=G\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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}$$
9	8	wfrlem3	$$⊢g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}\to \mathrm{dom}g\subseteq A$$
10	7 9	mprgbir	$$⊢\bigcup _{g\in \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)=G\left({f\upharpoonright }_{Pred\left(R,A,y\right)}\right)\right)\right\}}\mathrm{dom}g\subseteq A$$
11	6 10	eqsstri	$$⊢\mathrm{dom}F\subseteq A$$