Theorem dff1o4 5627

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 5624	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ Fun `' F /\ ran F = B ) )
2		3anass 1009	. 2 |- ( ( F Fn A /\ Fun `' F /\ ran F = B ) <-> ( F Fn A /\ ( Fun `' F /\ ran F = B ) ) )
3		df-rn 4765	. . . . . 6 |- ran F = dom `' F
4	3	eqeq1i 2242	. . . . 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 5360	. . . 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 1005   = wceq 1398   `'ccnv 4753   dom cdm 4754   ran crn 4755   Fun wfun 5351   Fn wfn 5352   -1-1-onto->wf1o 5356

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-rn 4765  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364

This theorem is referenced by:  f1ocnv  5632  f1oun  5639  f1o00  5656  f1oi  5659  f1osn  5661  f1ompt  5833  f1ofveu  6046  f1ocnvd  6265  f1o3d  6271  f1od2  6444  mapsnf1o2  6944  sbthlemi9  7248  xnn0nnen  10823  nninfctlemfo  12761  mhmf1o  13725  grpinvf1o  13825  ghmf1o  14028  rhmf1o  14413  hmeof1o2  15299