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}_h:\mathrm{dom}{adj}_h\underset{1-1\; onto}{⟶}\mathrm{dom}{adj}_h$$

Proof

Step	Hyp	Ref	Expression
1		funadj	$$⊢\mathrm{Fun}{adj}_h$$
2		funfn	$$⊢\mathrm{Fun}{adj}_h\leftrightarrow {adj}_{h}Fn\mathrm{dom}{adj}_h$$
3	1 2	mpbi	$$⊢{adj}_{h}Fn\mathrm{dom}{adj}_h$$
4		funcnvadj	$$⊢\mathrm{Fun}{{adj}_h}^{-1}$$
5		df-rn	$$⊢\mathrm{ran}{adj}_h=\mathrm{dom}{{adj}_h}^{-1}$$
6		cnvadj	$$⊢{{adj}_h}^{-1}={adj}_h$$
7	6	dmeqi	$$⊢\mathrm{dom}{{adj}_h}^{-1}=\mathrm{dom}{adj}_h$$
8	5 7	eqtri	$$⊢\mathrm{ran}{adj}_h=\mathrm{dom}{adj}_h$$
9		dff1o2	$$⊢{adj}_h:\mathrm{dom}{adj}_h\underset{1-1\; onto}{⟶}\mathrm{dom}{adj}_h\leftrightarrow \left({adj}_{h}Fn\mathrm{dom}{adj}_h\wedge \mathrm{Fun}{{adj}_h}^{-1}\wedge \mathrm{ran}{adj}_h=\mathrm{dom}{adj}_h\right)$$
10	3 4 8 9	mpbir3an	$$⊢{adj}_h:\mathrm{dom}{adj}_h\underset{1-1\; onto}{⟶}\mathrm{dom}{adj}_h$$