Metamath Proof Explorer


Theorem mapfset

Description: If B is a set, the value of the set exponentiation ( B ^m A ) is the class of all functions from A to B . Generalisation of mapvalg (which does not require ax-rep ) to arbitrary domains. Note that the class { f | f : A --> B } can only contain set-functions, as opposed to arbitrary class-functions. When A is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 ), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024)

Ref Expression
Assertion mapfset
|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) )

Proof

Step Hyp Ref Expression
1 vex
 |-  m e. _V
2 feq1
 |-  ( f = m -> ( f : A --> B <-> m : A --> B ) )
3 1 2 elab
 |-  ( m e. { f | f : A --> B } <-> m : A --> B )
4 simpr
 |-  ( ( m : A --> B /\ B e. V ) -> B e. V )
5 dmfex
 |-  ( ( m e. _V /\ m : A --> B ) -> A e. _V )
6 1 5 mpan
 |-  ( m : A --> B -> A e. _V )
7 6 adantr
 |-  ( ( m : A --> B /\ B e. V ) -> A e. _V )
8 4 7 elmapd
 |-  ( ( m : A --> B /\ B e. V ) -> ( m e. ( B ^m A ) <-> m : A --> B ) )
9 8 exbiri
 |-  ( m : A --> B -> ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) ) )
10 9 pm2.43b
 |-  ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) )
11 elmapi
 |-  ( m e. ( B ^m A ) -> m : A --> B )
12 10 11 impbid1
 |-  ( B e. V -> ( m : A --> B <-> m e. ( B ^m A ) ) )
13 3 12 syl5bb
 |-  ( B e. V -> ( m e. { f | f : A --> B } <-> m e. ( B ^m A ) ) )
14 13 eqrdv
 |-  ( B e. V -> { f | f : A --> B } = ( B ^m A ) )