Theorem f1ovi

Description: The identity relation is a one-to-one onto function on the universe. (Contributed by NM, 16-May-2004)

	Ref	Expression
Assertion	f1ovi	$$⊢\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{V}}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
2		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
3		dfrel3	$$⊢\mathrm{Rel}\mathrm{I}\leftrightarrow {\mathrm{I}\upharpoonright }_{\mathrm{V}}=\mathrm{I}$$
4	2 3	mpbi	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{V}}=\mathrm{I}$$
5		f1oeq1	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{V}}=\mathrm{I}\to \left(\left({\mathrm{I}\upharpoonright }_{\mathrm{V}}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\leftrightarrow \mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\right)$$
6	4 5	ax-mp	$$⊢\left({\mathrm{I}\upharpoonright }_{\mathrm{V}}\right):\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}\leftrightarrow \mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$
7	1 6	mpbi	$$⊢\mathrm{I}:\mathrm{V}\underset{1-1\; onto}{⟶}\mathrm{V}$$