This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 focdmex 
 |-  ( { 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 )