Theorem f1ofo 3803

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		dff1o3 3802	. 2 |- (F:A-1-1-onto->B <-> (F:A-onto->B /\ Fun `'F))
2	1	pm3.26bi 320	1 |- (F:A-1-1-onto->B -> F:A-onto->B)

Syntax hints:   -> wi 3  `'ccnv 3250  Fun wfun 3257  -onto->wfo 3261  -1-1-onto->wf1o 3262

This theorem is referenced by:  f1imacnv 3813  resin 3817  f1ococnv2 3819  f1dmex 3821  fo00 3826  isoini 4014  isofrlem 4015  isowe 4017  f1oweALT 4020  curry1 4193  curry2 4196  ncanth 4206  f1imaen 4563  en1 4567  ac6sfilem2 4589  ac6sfi 4591  canth2 4629  ssenen 4651  phplem4 4658  php3 4662  ssfi 4683  unifi 4701  fiint 4703  fodomfi 4709  unbenlem 7716  ruc 7761  infxpidmlem8 7771  infxpidmlem10 7773  infxpidmlem11 7774  infmap2lem1 7791  cnvunop 10122  counop 10125  idunop 10181  elunop2 10217  f1ofi 10778  eqindhome 11047  finsschain 11425  ordiso 11426  compfipin0lem 11492  compfipin0 11493  comptoppr 11495  conntoppr 11504  fbssint 11626  filfm 11706  fcluscomplem 11732  hmeocld 11961  ismtyhmeolem 12006

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278

Copyright terms: Public domain