Theorem dfatprc

Description: A function is not defined at a proper class. (Contributed by AV, 1-Sep-2022)

	Ref	Expression
Assertion	dfatprc	$$⊢\neg A\in \mathrm{V}\to \neg F\mathrm{defAt}A$$

Proof

Step	Hyp	Ref	Expression
1		prcnel	$$⊢\neg A\in \mathrm{V}\to \neg A\in \mathrm{dom}F$$
2	1	orcd	$$⊢\neg A\in \mathrm{V}\to \left(\neg A\in \mathrm{dom}F\vee \neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
3		ianor	$$⊢\neg \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)\leftrightarrow \left(\neg A\in \mathrm{dom}F\vee \neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
4		df-dfat	$$⊢F\mathrm{defAt}A\leftrightarrow \left(A\in \mathrm{dom}F\wedge \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
5	3 4	xchnxbir	$$⊢\neg F\mathrm{defAt}A\leftrightarrow \left(\neg A\in \mathrm{dom}F\vee \neg \mathrm{Fun}\left({F\upharpoonright }_{\left\{A\right\}}\right)\right)$$
6	2 5	sylibr	$$⊢\neg A\in \mathrm{V}\to \neg F\mathrm{defAt}A$$