Theorem f1f1orn 5583

Description: A one-to-one function maps one-to-one onto its range. (Contributed by NM, 4-Sep-2004.)

Assertion

Ref	Expression
f1f1orn	|- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )

Proof of Theorem f1f1orn

Step	Hyp	Ref	Expression
1		f1fn 5533	. 2 |- ( F : A -1-1-> B -> F Fn A )
2		df-f1 5323	. . 3 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
3	2	simprbi 275	. 2 |- ( F : A -1-1-> B -> Fun `' F )
4		f1orn 5582	. 2 |- ( F : A -1-1-onto-> ran F <-> ( F Fn A /\ Fun `' F ) )
5	1, 3, 4	sylanbrc 417	1 |- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )

Syntax hints:   -> wi 4   `'ccnv 4718   ran crn 4720   Fun wfun 5312   Fn wfn 5313   -->wf 5314   -1-1->wf1 5315   -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-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325

This theorem is referenced by:  f1ores  5587  f1cnv  5596  f1cocnv1  5602  f1ocnvfvrneq  5906  ssenen  7012  f1dmvrnfibi  7111  cc2lem  7452  4sqlem11  12924  xpsff1o2  13384  imasmndf1  13487  imasgrpf1  13649  conjsubgen  13815  imasrngf1  13920  imasringf1  14028  usgrf1o  15972  uspgrf1oedg  15974