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→ ℋ