Metamath Proof Explorer

Theorem hoif

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

Proof

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