Theorem fsetdmprc0

Description: The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024)

	Ref	Expression
Assertion	fsetdmprc0	$$⊢A\notin \mathrm{V}\to \left\{f|fFnA\right\}=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-nel	$$⊢A\notin \mathrm{V}\leftrightarrow \neg A\in \mathrm{V}$$
2		vex	$$⊢g\in \mathrm{V}$$
3	2	a1i	$$⊢gFnA\to g\in \mathrm{V}$$
4		id	$$⊢gFnA\to gFnA$$
5	3 4	fndmexd	$$⊢gFnA\to A\in \mathrm{V}$$
6	5	con3i	$$⊢\neg A\in \mathrm{V}\to \neg gFnA$$
7	1 6	sylbi	$$⊢A\notin \mathrm{V}\to \neg gFnA$$
8	7	alrimiv	$$⊢A\notin \mathrm{V}\to \forall g\neg gFnA$$
9		fneq1	$$⊢f=g\to \left(fFnA\leftrightarrow gFnA\right)$$
10	9	ab0w	$$⊢\left\{f|fFnA\right\}=\varnothing \leftrightarrow \forall g\neg gFnA$$
11	8 10	sylibr	$$⊢A\notin \mathrm{V}\to \left\{f|fFnA\right\}=\varnothing$$