Metamath Proof Explorer


Theorem dff1o4

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

Ref Expression
Assertion dff1o4 F : A 1-1 onto B F Fn A F -1 Fn B

Proof

Step Hyp Ref Expression
1 dff1o2 F : A 1-1 onto B F Fn A Fun F -1 ran F = B
2 3anass F Fn A Fun F -1 ran F = B F Fn A Fun F -1 ran F = B
3 df-rn ran F = dom F -1
4 3 eqeq1i ran F = B dom F -1 = B
5 4 anbi2i Fun F -1 ran F = B Fun F -1 dom F -1 = B
6 df-fn F -1 Fn B Fun F -1 dom F -1 = B
7 5 6 bitr4i Fun F -1 ran F = B F -1 Fn B
8 7 anbi2i F Fn A Fun F -1 ran F = B F Fn A F -1 Fn B
9 1 2 8 3bitri F : A 1-1 onto B F Fn A F -1 Fn B