Metamath Proof Explorer


Theorem 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 V A B V f | f : A B V

Proof

Step Hyp Ref Expression
1 n0 A a a A
2 feq1 f = m f : A B m : A B
3 2 cbvabv f | f : A B = m | m : A B
4 fveq1 g = n g a = n a
5 4 cbvmptv g f | f : A B g a = n f | f : A B n a
6 3 5 fsetfocdm A V a A g f | f : A B g a : f | f : A B onto B
7 fornex f | f : A B V g f | f : A B g a : f | f : A B onto B B V
8 6 7 syl5com A V a A f | f : A B V B V
9 8 nelcon3d A V a A B V f | f : A B V
10 9 expcom a A A V B V f | f : A B V
11 10 exlimiv a a A A V B V f | f : A B V
12 1 11 sylbi A A V B V f | f : A B V
13 12 impcom A V A B V f | f : A B V
14 13 imp A V A B V f | f : A B V