Theorem nfunsn

Description: If the restriction of a class to a singleton is not a function, then its value is the empty set. (An artifact of our function value definition.) (Contributed by NM, 8-Aug-2010) (Proof shortened by Andrew Salmon, 22-Oct-2011)

	Ref	Expression
Assertion	nfunsn	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eumo	$$⊢\exists !yAFy\to {\exists }^{*}yAFy$$
2		vex	$$⊢y\in \mathrm{V}$$
3	2	brresi	$$⊢x\left({F\upharpoonright }_{\left\{A\right\}}\right)y\leftrightarrow \left(x\in \left\{A\right\}\wedge xFy\right)$$
4		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
5		breq1	$$⊢x=A\to \left(xFy\leftrightarrow AFy\right)$$
6	4 5	sylbi	$$⊢x\in \left\{A\right\}\to \left(xFy\leftrightarrow AFy\right)$$
7	6	biimpa	$$⊢\left(x\in \left\{A\right\}\wedge xFy\right)\to AFy$$
8	3 7	sylbi	$$⊢x\left({F\upharpoonright }_{\left\{A\right\}}\right)y\to AFy$$
9	8	moimi	$$⊢{\exists }^{*}yAFy\to {\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
10	1 9	syl	$$⊢\exists !yAFy\to {\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
11		tz6.12-2	$$⊢\neg \exists !yAFy\to F\left(A\right)=\varnothing$$
12	10 11	nsyl4	$$⊢\neg F\left(A\right)=\varnothing \to {\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
13	12	alrimiv	$$⊢\neg F\left(A\right)=\varnothing \to \forall x{\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y$$
14		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
15	13 14	jctil	$$⊢\neg F\left(A\right)=\varnothing \to \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge \forall x{\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)$$
16		dffun6	$$⊢\mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\leftrightarrow \left(\mathrm{Rel}\left({F\upharpoonright }_{\left\{A\right\}}\right)\wedge \forall x{\exists }^{*}yx\left({F\upharpoonright }_{\left\{A\right\}}\right)y\right)$$
17	15 16	sylibr	$$⊢\neg F\left(A\right)=\varnothing \to \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)$$
18	17	con1i	$$⊢\neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\to F\left(A\right)=\varnothing$$