Theorem f1ofo 3701

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 3700	. 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 3175  Fun wfun 3182  -onto->wfo 3186  -1-1-onto->wf1o 3187

This theorem is referenced by:  f1imacnv 3711  f1ococnv2 3714  f1dmex 3716  fo00 3721  isoini 3906  isofrlem 3907  isowe 3909  f1oweALT 3912  ncanth 3914  curry1 4104  f1imaen 4428  en1 4432  canth2 4490  ssenen 4510  phplem4 4517  php3 4521  php3OLD 4522  ssfi 4547  ssfiOLD 4548  unifiOLD 4570  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  unbenlem 7505  ruc 7550  infxpidmlem8 7560  infxpidmlem10 7562  infxpidmlem11 7563  infmap2lem1 7581  cnvunopt 9837  counopt 9840  idunop 9897  elunop2t 9933  eqindhome 10527

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056  df-f 3200  df-f1 3201  df-fo 3202  df-f1o 3203

Copyright terms: Public domain