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

Metamath Proof Explorer

Theorem mapfoss

Description: The value of the set exponentiation ( B ^m A ) is a superset of the set of all functions from A onto B . (Contributed by AV, 7-Aug-2024)

Ref Expression
Assertion mapfoss 
|- { f | f : A -onto-> B } C_ ( B ^m A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  m e. _V
2 foeq1 
 |-  ( f = m -> ( f : A -onto-> B <-> m : A -onto-> B ) )
3 1 2 elab 
 |-  ( m e. { f | f : A -onto-> B } <-> m : A -onto-> B )
4 fof 
 |-  ( m : A -onto-> B -> m : A --> B )
5 forn 
 |-  ( m : A -onto-> B -> ran m = B )
6 1 rnex 
 |-  ran m e. _V
7 5 6 eqeltrrdi 
 |-  ( m : A -onto-> B -> B e. _V )
8 dmfex 
 |-  ( ( m e. _V /\ m : A --> B ) -> A e. _V )
9 1 4 8 sylancr 
 |-  ( m : A -onto-> B -> A e. _V )
10 7 9 elmapd 
 |-  ( m : A -onto-> B -> ( m e. ( B ^m A ) <-> m : A --> B ) )
11 4 10 mpbird 
 |-  ( m : A -onto-> B -> m e. ( B ^m A ) )
12 3 11 sylbi 
 |-  ( m e. { f | f : A -onto-> B } -> m e. ( B ^m A ) )
13 12 ssriv 
 |-  { f | f : A -onto-> B } C_ ( B ^m A )