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

Metamath Proof Explorer

Theorem mapsnconst

Description: Every singleton map is a constant function. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses mapsncnv.s 
|- S = { X }
mapsncnv.b 
|- B e. _V
mapsncnv.x 
|- X e. _V
Assertion mapsnconst 
|- ( F e. ( B ^m S ) -> F = ( S X. { ( F ` X ) } ) )

Proof

Step Hyp Ref Expression
1 mapsncnv.s 
 |-  S = { X }
2 mapsncnv.b 
 |-  B e. _V
3 mapsncnv.x 
 |-  X e. _V
4 snex 
 |-  { X } e. _V
5 2 4 elmap 
 |-  ( F e. ( B ^m { X } ) <-> F : { X } --> B )
6 3 fsn2 
 |-  ( F : { X } --> B <-> ( ( F ` X ) e. B /\ F = { <. X , ( F ` X ) >. } ) )
7 6 simprbi 
 |-  ( F : { X } --> B -> F = { <. X , ( F ` X ) >. } )
8 1 xpeq1i 
 |-  ( S X. { ( F ` X ) } ) = ( { X } X. { ( F ` X ) } )
9 fvex 
 |-  ( F ` X ) e. _V
10 3 9 xpsn 
 |-  ( { X } X. { ( F ` X ) } ) = { <. X , ( F ` X ) >. }
11 8 10 eqtr2i 
 |-  { <. X , ( F ` X ) >. } = ( S X. { ( F ` X ) } )
12 7 11 eqtrdi 
 |-  ( F : { X } --> B -> F = ( S X. { ( F ` X ) } ) )
13 5 12 sylbi 
 |-  ( F e. ( B ^m { X } ) -> F = ( S X. { ( F ` X ) } ) )
14 1 oveq2i 
 |-  ( B ^m S ) = ( B ^m { X } )
15 13 14 eleq2s 
 |-  ( F e. ( B ^m S ) -> F = ( S X. { ( F ` X ) } ) )