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