Theorem adj1o

Description: The adjoint function maps one-to-one onto its domain. (Contributed by NM, 15-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	adj1o	⊢ adjℎ : dom adjℎ –1-1-onto→ dom adjℎ

Proof

Step	Hyp	Ref	Expression
1		funadj	⊢ Fun adjℎ
2		funfn	⊢ ( Fun adjℎ ↔ adjℎ Fn dom adjℎ )
3	1 2	mpbi	⊢ adjℎ Fn dom adjℎ
4		funcnvadj	⊢ Fun ◡ adjℎ
5		df-rn	⊢ ran adjℎ = dom ◡ adjℎ
6		cnvadj	⊢ ◡ adjℎ = adjℎ
7	6	dmeqi	⊢ dom ◡ adjℎ = dom adjℎ
8	5 7	eqtri	⊢ ran adjℎ = dom adjℎ
9		dff1o2	⊢ ( adjℎ : dom adjℎ –1-1-onto→ dom adjℎ ↔ ( adjℎ Fn dom adjℎ ∧ Fun ◡ adjℎ ∧ ran adjℎ = dom adjℎ ) )
10	3 4 8 9	mpbir3an	⊢ adjℎ : dom adjℎ –1-1-onto→ dom adjℎ