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 : ℋ –1-1-onto→ ℋ

Proof

Step Hyp Ref Expression
1 f1oi ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ
2 dfiop2 Iop = ( I ↾ ℋ )
3 f1oeq1 ( Iop = ( I ↾ ℋ ) → ( Iop : ℋ –1-1-onto→ ℋ ↔ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ ) )
4 2 3 ax-mp ( Iop : ℋ –1-1-onto→ ℋ ↔ ( I ↾ ℋ ) : ℋ –1-1-onto→ ℋ )
5 1 4 mpbir Iop : ℋ –1-1-onto→ ℋ