Metamath Proof Explorer


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