Metamath Proof Explorer

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 : dom ⁡ adj h ⟶ 1-1 onto dom ⁡ adj h

Proof

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