Theorem hoif

Description: Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	hoif	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
2		dfiop2	$$⊢I_{\mathrm{op}}={\mathrm{I}\upharpoonright }_{\mathscr{H}}$$
3		f1oeq1	$$⊢I_{\mathrm{op}}={\mathrm{I}\upharpoonright }_{\mathscr{H}}\to \left(I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\right)$$
4	2 3	ax-mp	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\mathscr{H}}\right):\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$
5	1 4	mpbir	$$⊢I_{\mathrm{op}}:\mathscr{H}\underset{1-1\; onto}{⟶}\mathscr{H}$$