Theorem dff1o4 5582

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

Assertion

Ref	Expression
dff1o4	|- ( F : A -1-1-onto-> B <-> ( F Fn A /\ `' F Fn B ) )

Proof of Theorem dff1o4

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

Syntax hints:   /\ wa 104   <-> wb 105   /\ w3a 1002   = wceq 1395   `'ccnv 4718   dom cdm 4719   ran crn 4720   Fun wfun 5312   Fn wfn 5313   -1-1-onto->wf1o 5317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-rn 4730  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325

This theorem is referenced by:  f1ocnv  5587  f1oun  5594  f1o00  5610  f1oi  5613  f1osn  5615  f1ompt  5788  f1ofveu  5995  f1ocnvd  6214  f1od2  6387  mapsnf1o2  6851  sbthlemi9  7143  xnn0nnen  10671  nninfctlemfo  12576  mhmf1o  13518  grpinvf1o  13618  ghmf1o  13827  rhmf1o  14147  hmeof1o2  14997