Theorem f1ofo 3686

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 3685	. 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 3164  Fun wfun 3171  -onto->wfo 3175  -1-1-onto->wf1o 3176

This theorem is referenced by:  f1imacnv 3696  f1ococnv2 3699  f1dmex 3701  fo00 3706  isoini 3891  isofrlem 3892  isowe 3894  f1oweALT 3897  ncanth 3899  curry1 4088  f1imaen 4409  en1 4413  canth2 4470  ssenen 4490  phplem4 4497  php3 4501  ssfi 4521  unifi 4538  fiint 4540  fodomfi 4546  unbenlem 7455  ruc 7500  infxpidmlem8 7510  infxpidmlem10 7512  infxpidmlem11 7513  infmap2lem1 7529  cnvunopt 9781  counopt 9784  idunop 9841  elunop2t 9876

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-f 3189  df-f1 3190  df-fo 3191  df-f1o 3192

Copyright terms: Public domain