fsetprcnex

Description: The class of all functions from a nonempty set A into a proper class B is not a set. If one of the preconditions is not fufilled, then { f | f : A --> B } is a set, see fsetdmprc0 for A e/V , fset0 for A = (/) , and fsetex for B e. V , see also fsetexb . (Contributed by AV, 14-Sep-2024) (Proof shortened by BJ, 15-Sep-2024)

		Ref	Expression
	Assertion	fsetprcnex	$⊢ ((A \in V \land A \neq \emptyset) \land B \notin V) \to \{f \| f : A ⟶ B\} \notin V$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ A \neq \emptyset \leftrightarrow \exists a a \in A$
2		feq1	$⊢ f = m \to (f : A ⟶ B \leftrightarrow m : A ⟶ B)$
3	2	cbvabv	$⊢ \{f \| f : A ⟶ B\} = \{m \| m : A ⟶ B\}$
4		fveq1	$⊢ g = n \to g (a) = n (a)$
5	4	cbvmptv	$⊢ (g \in \{f \| f : A ⟶ B\} ⟼ g (a)) = (n \in \{f \| f : A ⟶ B\} ⟼ n (a))$
6	3 5	fsetfocdm	$⊢ (A \in V \land a \in A) \to (g \in \{f \| f : A ⟶ B\} ⟼ g (a)) : \{f \| f : A ⟶ B\} \underset{onto}{⟶} B$
7		focdmex	$⊢ \{f \| f : A ⟶ B\} \in V \to ((g \in \{f \| f : A ⟶ B\} ⟼ g (a)) : \{f \| f : A ⟶ B\} \underset{onto}{⟶} B \to B \in V)$
8	6 7	syl5com	$⊢ (A \in V \land a \in A) \to (\{f \| f : A ⟶ B\} \in V \to B \in V)$
9	8	nelcon3d	$⊢ (A \in V \land a \in A) \to (B \notin V \to \{f \| f : A ⟶ B\} \notin V)$
10	9	expcom	$⊢ a \in A \to (A \in V \to (B \notin V \to \{f \| f : A ⟶ B\} \notin V))$
11	10	exlimiv	$⊢ \exists a a \in A \to (A \in V \to (B \notin V \to \{f \| f : A ⟶ B\} \notin V))$
12	1 11	sylbi	$⊢ A \neq \emptyset \to (A \in V \to (B \notin V \to \{f \| f : A ⟶ B\} \notin V))$
13	12	impcom	$⊢ (A \in V \land A \neq \emptyset) \to (B \notin V \to \{f \| f : A ⟶ B\} \notin V)$
14	13	imp	$⊢ ((A \in V \land A \neq \emptyset) \land B \notin V) \to \{f \| f : A ⟶ B\} \notin V$

Metamath Proof Explorer

Theorem fsetprcnex

Proof