Theorem setrec2lem2

Description: Lemma for setrec2 . The functional part of F is a function. (Contributed by Emmett Weisz, 6-Mar-2021) (New usage is discouraged.)

	Ref	Expression
Assertion	setrec2lem2	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$
2		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
3		eqeq2	$$⊢z=F\left(x\right)\to \left(y=z\leftrightarrow y=F\left(x\right)\right)$$
4	3	imbi2d	$$⊢z=F\left(x\right)\to \left(\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)\leftrightarrow \left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=F\left(x\right)\right)\right)$$
5	4	albidv	$$⊢z=F\left(x\right)\to \left(\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)\leftrightarrow \forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=F\left(x\right)\right)\right)$$
6	2 5	spcev	$$⊢\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=F\left(x\right)\right)\to \exists z\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)$$
7		vex	$$⊢y\in \mathrm{V}$$
8	7	brresi	$$⊢x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\leftrightarrow \left(x\in \left\{x|\exists !yxFy\right\}\wedge xFy\right)$$
9		abid	$$⊢x\in \left\{x|\exists !yxFy\right\}\leftrightarrow \exists !yxFy$$
10		tz6.12-1	$$⊢\left(xFy\wedge \exists !yxFy\right)\to F\left(x\right)=y$$
11	10	ancoms	$$⊢\left(\exists !yxFy\wedge xFy\right)\to F\left(x\right)=y$$
12	9 11	sylanb	$$⊢\left(x\in \left\{x|\exists !yxFy\right\}\wedge xFy\right)\to F\left(x\right)=y$$
13	12	eqcomd	$$⊢\left(x\in \left\{x|\exists !yxFy\right\}\wedge xFy\right)\to y=F\left(x\right)$$
14	8 13	sylbi	$$⊢x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=F\left(x\right)$$
15	6 14	mpg	$$⊢\exists z\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)$$
16	15	ax-gen	$$⊢\forall x\exists z\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}xF$$
18		nfab1	$$⊢\underset{\_}{Ⅎ}x\left\{x|\exists !yxFy\right\}$$
19	17 18	nfres	$$⊢\underset{\_}{Ⅎ}x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}yF$$
21		nfeu1	$$⊢Ⅎy\exists !yxFy$$
22	21	nfab	$$⊢\underset{\_}{Ⅎ}y\left\{x|\exists !yxFy\right\}$$
23	20 22	nfres	$$⊢\underset{\_}{Ⅎ}y\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}z\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$
25	19 23 24	dffun3f	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\leftrightarrow \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)\wedge \forall x\exists z\forall y\left(x\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)y\to y=z\right)\right)$$
26	1 16 25	mpbir2an	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{x|\exists !yxFy\right\}}\right)$$