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 
|- adjh : dom adjh -1-1-onto-> dom adjh

Proof

Step Hyp Ref Expression
1 funadj 
 |-  Fun adjh
2 funfn 
 |-  ( Fun adjh <-> adjh Fn dom adjh )
3 1 2 mpbi 
 |-  adjh Fn dom adjh
4 funcnvadj 
 |-  Fun `' adjh
5 df-rn 
 |-  ran adjh = dom `' adjh
6 cnvadj 
 |-  `' adjh = adjh
7 6 dmeqi 
 |-  dom `' adjh = dom adjh
8 5 7 eqtri 
 |-  ran adjh = dom adjh
9 dff1o2 
 |-  ( adjh : dom adjh -1-1-onto-> dom adjh <-> ( adjh Fn dom adjh /\ Fun `' adjh /\ ran adjh = dom adjh ) )
10 3 4 8 9 mpbir3an 
 |-  adjh : dom adjh -1-1-onto-> dom adjh