![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1f1orn | Structured version Visualization version GIF version |
Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.) |
Ref | Expression |
---|---|
f1f1orn | β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran πΉ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1fn 6740 | . 2 β’ (πΉ:π΄β1-1βπ΅ β πΉ Fn π΄) | |
2 | df-f1 6502 | . . 3 β’ (πΉ:π΄β1-1βπ΅ β (πΉ:π΄βΆπ΅ β§ Fun β‘πΉ)) | |
3 | 2 | simprbi 498 | . 2 β’ (πΉ:π΄β1-1βπ΅ β Fun β‘πΉ) |
4 | f1orn 6795 | . 2 β’ (πΉ:π΄β1-1-ontoβran πΉ β (πΉ Fn π΄ β§ Fun β‘πΉ)) | |
5 | 1, 3, 4 | sylanbrc 584 | 1 β’ (πΉ:π΄β1-1βπ΅ β πΉ:π΄β1-1-ontoβran πΉ) |
Copyright terms: Public domain | W3C validator |