Description: The mapping of unary (endo)functions is a one-to-one function onto the set of endofunctions. (Contributed by AV, 19-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | 1arymaptfv.h | |- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) |
|
Assertion | 1arymaptf1o | |- ( X e. V -> H : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1arymaptfv.h | |- H = ( h e. ( 1 -aryF X ) |-> ( x e. X |-> ( h ` { <. 0 , x >. } ) ) ) |
|
2 | 1 | 1arymaptf1 | |- ( X e. V -> H : ( 1 -aryF X ) -1-1-> ( X ^m X ) ) |
3 | 1 | 1arymaptfo | |- ( X e. V -> H : ( 1 -aryF X ) -onto-> ( X ^m X ) ) |
4 | df-f1o | |- ( H : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) <-> ( H : ( 1 -aryF X ) -1-1-> ( X ^m X ) /\ H : ( 1 -aryF X ) -onto-> ( X ^m X ) ) ) |
|
5 | 2 3 4 | sylanbrc | |- ( X e. V -> H : ( 1 -aryF X ) -1-1-onto-> ( X ^m X ) ) |