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

Metamath Proof Explorer

Theorem funcnvcnv

Description: The double converse of a function is a function. (Contributed by NM, 21-Sep-2004)

		Ref	Expression
	Assertion	funcnvcnv	$⊢ Fun A \to Fun {A^{-1}}^{-1}$

Step	Hyp	Ref	Expression
1		cnvcnvss	$⊢ {A^{-1}}^{-1} \subseteq A$
2		funss	$⊢ {A^{-1}}^{-1} \subseteq A \to (Fun A \to Fun {A^{-1}}^{-1})$
3	1 2	ax-mp	$⊢ Fun A \to Fun {A^{-1}}^{-1}$