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	⊢ Fun ◡ adjℎ

Proof

Step	Hyp	Ref	Expression
1		funadj	⊢ Fun adjℎ
2		cnvadj	⊢ ◡ adjℎ = adjℎ
3	2	funeqi	⊢ ( Fun ◡ adjℎ ↔ Fun adjℎ )
4	1 3	mpbir	⊢ Fun ◡ adjℎ