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 e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. a a e. 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 e. { f | f : A --> B } |-> ( g ` a ) ) = ( n e. { f | f : A --> B } |-> ( n ` a ) )
6	3 5	fsetfocdm	|- ( ( A e. V /\ a e. A ) -> ( g e. { f | f : A --> B } |-> ( g ` a ) ) : { f | f : A --> B } -onto-> B )
7		fornex	|- ( { f | f : A --> B } e. _V -> ( ( g e. { f | f : A --> B } |-> ( g ` a ) ) : { f | f : A --> B } -onto-> B -> B e. _V ) )
8	6 7	syl5com	|- ( ( A e. V /\ a e. A ) -> ( { f | f : A --> B } e. _V -> B e. _V ) )
9	8	nelcon3d	|- ( ( A e. V /\ a e. A ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
10	9	expcom	|- ( a e. A -> ( A e. V -> ( B e/ _V -> { f | f : A --> B } e/ _V ) ) )
11	10	exlimiv	|- ( E. a a e. A -> ( A e. V -> ( B e/ _V -> { f | f : A --> B } e/ _V ) ) )
12	1 11	sylbi	|- ( A =/= (/) -> ( A e. V -> ( B e/ _V -> { f | f : A --> B } e/ _V ) ) )
13	12	impcom	|- ( ( A e. V /\ A =/= (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
14	13	imp	|- ( ( ( A e. V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )