Theorem funcnvadj

Description: The converse of the adjoint function is a function. (Contributed by NM, 25-Jan-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	funcnvadj	$$⊢\mathrm{Fun}{{adj}_h}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		funadj	$$⊢\mathrm{Fun}{adj}_h$$
2		cnvadj	$$⊢{{adj}_h}^{-1}={adj}_h$$
3	2	funeqi	$$⊢\mathrm{Fun}{{adj}_h}^{-1}\leftrightarrow \mathrm{Fun}{adj}_h$$
4	1 3	mpbir	$$⊢\mathrm{Fun}{{adj}_h}^{-1}$$