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 ) } ) )