Theorem f1ofo 3771

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 3770	. 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 3224  Fun wfun 3231  -onto->wfo 3235  -1-1-onto->wf1o 3236

This theorem is referenced by:  f1imacnv 3781  f1ococnv2 3784  f1dmex 3786  fo00 3791  isoini 3976  isofrlem 3977  isowe 3979  f1oweALT 3982  ncanth 3984  curry1 4208  curry2 4211  f1imaen 4509  en1 4513  canth2 4571  ssenen 4593  phplem4 4600  php3 4604  ssfi 4625  unifi 4642  fiint 4644  fodomfi 4650  unbenlem 7629  ruc 7674  infxpidmlem8 7684  infxpidmlem10 7686  infxpidmlem11 7687  infmap2lem1 7704  cnvunop 9960  counop 9963  idunop 10019  elunop2 10055  eqindhome 10677

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-sb 1205  df-clab 1500  df-cleq 1505  df-clel 1508  df-in 2095  df-ss 2097  df-f 3249  df-f1 3250  df-fo 3251  df-f1o 3252

Copyright terms: Public domain