Description: Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | hoif | |- Iop : ~H -1-1-onto-> ~H |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oi | |- ( _I |` ~H ) : ~H -1-1-onto-> ~H |
|
2 | dfiop2 | |- Iop = ( _I |` ~H ) |
|
3 | f1oeq1 | |- ( Iop = ( _I |` ~H ) -> ( Iop : ~H -1-1-onto-> ~H <-> ( _I |` ~H ) : ~H -1-1-onto-> ~H ) ) |
|
4 | 2 3 | ax-mp | |- ( Iop : ~H -1-1-onto-> ~H <-> ( _I |` ~H ) : ~H -1-1-onto-> ~H ) |
5 | 1 4 | mpbir | |- Iop : ~H -1-1-onto-> ~H |