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	⊢ Fun I

Proof

Step	Hyp	Ref	Expression
1		reli	⊢ Rel I
2		relcnv	⊢ Rel ◡ I
3		coi2	⊢ ( Rel ◡ I → ( I ∘ ◡ I ) = ◡ I )
4	2 3	ax-mp	⊢ ( I ∘ ◡ I ) = ◡ I
5		cnvi	⊢ ◡ I = I
6	4 5	eqtri	⊢ ( I ∘ ◡ I ) = I
7	6	eqimssi	⊢ ( I ∘ ◡ I ) ⊆ I
8		df-fun	⊢ ( Fun I ↔ ( Rel I ∧ ( I ∘ ◡ I ) ⊆ I ) )
9	1 7 8	mpbir2an	⊢ Fun I