Theorem dff1o4 5579

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 5576	. 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 4729	. . . . . 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 5320	. . . 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 4717   dom cdm 4718   ran crn 4719   Fun wfun 5311   Fn wfn 5312   -1-1-onto->wf1o 5316

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 4729  df-fn 5320  df-f 5321  df-f1 5322  df-fo 5323  df-f1o 5324

This theorem is referenced by:  f1ocnv  5584  f1oun  5591  f1o00  5607  f1oi  5610  f1osn  5612  f1ompt  5785  f1ofveu  5988  f1ocnvd  6206  f1od2  6379  mapsnf1o2  6841  sbthlemi9  7128  xnn0nnen  10654  nninfctlemfo  12556  mhmf1o  13498  grpinvf1o  13598  ghmf1o  13807  rhmf1o  14126  hmeof1o2  14976