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