Theorem f1ofo 3695

Description: A one-to-one onto function is an onto function.

Assertion

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

Proof of Theorem f1ofo

Step	Hyp	Ref	Expression
1		f1o3 3694	. 2 |- (F:A-1-1-onto->B <-> (F:A-onto->B /\ Fun `'F))
2	1	pm3.26bi 322	1 |- (F:A-1-1-onto->B -> F:A-onto->B)

Syntax hints:   -> wi 3  `'ccnv 3169  Fun wfun 3176  -onto->wfo 3180  -1-1-onto->wf1o 3181

This theorem is referenced by:  f1imacnv 3705  f1ococnv2 3708  f1dmex 3710  fo00 3715  isoini 3900  isofrlem 3901  isowe 3903  f1oweALT 3906  ncanth 3908  curry1 4098  f1imaen 4422  en1 4426  canth2 4484  ssenen 4504  phplem4 4511  php3 4515  php3OLD 4516  ssfi 4537  ssfiOLD 4538  unifiOLD 4557  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  unbenlem 7504  ruc 7549  infxpidmlem8 7559  infxpidmlem10 7561  infxpidmlem11 7562  infmap2lem1 7579  cnvunopt 9842  counopt 9845  idunop 9902  elunop2t 9938  eqindhome 10541

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-f 3194  df-f1 3195  df-fo 3196  df-f1o 3197

Copyright terms: Public domain