Theorem f1ofo 2806

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 2805	. 2 ⊢ (F:A–1-1-onto→B ↔ (F:A–onto→B ∧ Fun ◡F))
2	1	pm3.26bd 259	1 ⊢ (F:A–1-1-onto→B → F:A–onto→B)

Syntax hints:   → wi 2  ^◡ccnv 2409  Fun wfun 2416  –onto→wfo 2420  –1-1-onto→wf1o 2421

This theorem is referenced by:  f1imacnv 2814  f1dmex 2819  isoini 2938  isofrlem 2939  isowe 2941  ncanth 2946  f1imaen 3327  en1 3331  ssenen 3399  phplem5 3407  php3 3411  infxpidmlem8 4940  infxpidmlem10 4942  infxpidmlem11 4943  infmap2lem1 4951

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437

metamath.org