Theorem dmadjrn

Description: The adjoint of an operator belongs to the adjoint function's domain. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	dmadjrn	|- ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )

Proof

Step	Hyp	Ref	Expression
1		adj1o	|- adjh : dom adjh -1-1-onto-> dom adjh
2		f1of	|- ( adjh : dom adjh -1-1-onto-> dom adjh -> adjh : dom adjh --> dom adjh )
3	1 2	ax-mp	|- adjh : dom adjh --> dom adjh
4	3	ffvelrni	|- ( T e. dom adjh -> ( adjh ` T ) e. dom adjh )