Theorem mapsnf1o2

Description: Explicit bijection between a set and its singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mapsncnv.s	|- S = { X }
2		mapsncnv.b	|- B e. _V
3		mapsncnv.x	|- X e. _V
4		mapsncnv.f	|- F = ( x e. ( B ^m S ) |-> ( x ` X ) )
5		fvex	|- ( x ` X ) e. _V
6	5 4	fnmpti	|- F Fn ( B ^m S )
7		snex	|- { X } e. _V
8	1 7	eqeltri	|- S e. _V
9		snex	|- { y } e. _V
10	8 9	xpex	|- ( S X. { y } ) e. _V
11	1 2 3 4	mapsncnv	|- `' F = ( y e. B |-> ( S X. { y } ) )
12	10 11	fnmpti	|- `' F Fn B
13		dff1o4	|- ( F : ( B ^m S ) -1-1-onto-> B <-> ( F Fn ( B ^m S ) /\ `' F Fn B ) )
14	6 12 13	mpbir2an	|- F : ( B ^m S ) -1-1-onto-> B