Theorem funcnvcnv

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

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

Proof

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