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

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 bitrid 
 |-  ( 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 ) )