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