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 V \to \{f \| f Fn A\} = \emptyset$

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

Metamath Proof Explorer