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 Fn B ) )

Proof

Step Hyp Ref Expression
1 dff1o2 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ Fun `' F /\ ran F = B ) )
2 3anass 
 |-  ( ( F Fn A /\ Fun `' F /\ ran F = B ) <-> ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) )
3 df-rn 
 |-  ran F = dom `' F
4 3 eqeq1i 
 |-  ( ran F = B <-> dom `' F = B )
5 4 anbi2i 
 |-  ( ( Fun `' F /\ ran F = B ) <-> ( Fun `' F /\ dom `' F = B ) )
6 df-fn 
 |-  ( `' F Fn B <-> ( Fun `' F /\ dom `' F = B ) )
7 5 6 bitr4i 
 |-  ( ( Fun `' F /\ ran F = B ) <-> `' F Fn B )
8 7 anbi2i 
 |-  ( ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) <-> ( F Fn A /\ `' F Fn B ) )
9 1 2 8 3bitri 
 |-  ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )