This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fococnv2

Description: The composition of an onto function and its converse. (Contributed by Stefan O'Rear, 12-Feb-2015)

		Ref	Expression
	Assertion	fococnv2	$⊢ F : A \underset{onto}{⟶} B \to F \circ F^{-1} = {I ↾}_{B}$

Step	Hyp	Ref	Expression
1		fofun	$⊢ F : A \underset{onto}{⟶} B \to Fun F$
2		funcocnv2	$⊢ Fun F \to F \circ F^{-1} = {I ↾}_{ran F}$
3	1 2	syl	$⊢ F : A \underset{onto}{⟶} B \to F \circ F^{-1} = {I ↾}_{ran F}$
4		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
5	4	reseq2d	$⊢ F : A \underset{onto}{⟶} B \to {I ↾}_{ran F} = {I ↾}_{B}$
6	3 5	eqtrd	$⊢ F : A \underset{onto}{⟶} B \to F \circ F^{-1} = {I ↾}_{B}$