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	$⊢ I : V \underset{1-1 onto}{⟶} V$

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

Metamath Proof Explorer