Metamath Proof Explorer


Theorem dff1o5

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o5 F : A 1-1 onto B F : A 1-1 B ran F = B

Proof

Step Hyp Ref Expression
1 df-f1o F : A 1-1 onto B F : A 1-1 B F : A onto B
2 dffo2 F : A onto B F : A B ran F = B
3 f1f F : A 1-1 B F : A B
4 3 biantrurd F : A 1-1 B ran F = B F : A B ran F = B
5 2 4 bitr4id F : A 1-1 B F : A onto B ran F = B
6 5 pm5.32i F : A 1-1 B F : A onto B F : A 1-1 B ran F = B
7 1 6 bitri F : A 1-1 onto B F : A 1-1 B ran F = B