Theorem funi

Description: The identity relation is a function. Part of Theorem 10.4 of Quine p. 65. See also idfn . (Contributed by NM, 30-Apr-1998)

	Ref	Expression
Assertion	funi	$$⊢\mathrm{Fun}\mathrm{I}$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2		relcnv	$$⊢\mathrm{Rel}{\mathrm{I}}^{-1}$$
3		coi2	$$⊢\mathrm{Rel}{\mathrm{I}}^{-1}\to \mathrm{I}\circ {\mathrm{I}}^{-1}={\mathrm{I}}^{-1}$$
4	2 3	ax-mp	$$⊢\mathrm{I}\circ {\mathrm{I}}^{-1}={\mathrm{I}}^{-1}$$
5		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
6	4 5	eqtri	$$⊢\mathrm{I}\circ {\mathrm{I}}^{-1}=\mathrm{I}$$
7	6	eqimssi	$$⊢\mathrm{I}\circ {\mathrm{I}}^{-1}\subseteq \mathrm{I}$$
8		df-fun	$$⊢\mathrm{Fun}\mathrm{I}\leftrightarrow \left(\mathrm{Rel}\mathrm{I}\wedge \mathrm{I}\circ {\mathrm{I}}^{-1}\subseteq \mathrm{I}\right)$$
9	1 7 8	mpbir2an	$$⊢\mathrm{Fun}\mathrm{I}$$