MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fofn Structured version   Unicode version

Theorem fofn 5617
Description: An onto mapping is a function on its domain. (Contributed by NM, 16-Dec-2008.)
Assertion
Ref Expression
fofn  |-  ( F : A -onto-> B  ->  F  Fn  A )

Proof of Theorem fofn
StepHypRef Expression
1 fof 5615 . 2  |-  ( F : A -onto-> B  ->  F : A --> B )
2 ffn 5554 . 2  |-  ( F : A --> B  ->  F  Fn  A )
31, 2syl 16 1  |-  ( F : A -onto-> B  ->  F  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Fn wfn 5408   -->wf 5409   -onto->wfo 5411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337  df-f 5417  df-fo 5419
This theorem is referenced by:  fodmrnu  5623  foun  5654  fo00  5669  cbvfo  5988  foeqcnvco  5993  canth  6044  1stcof  6599  2ndcof  6600  df1st2  6654  df2nd2  6655  1stconst  6656  2ndconst  6657  fsplit  6672  smoiso2  6822  fodomfi  7582  brwdom2  7780  fodomfi2  8222  fpwwe  8805  imasaddfnlem  14458  imasvscafn  14467  imasleval  14471  dmaf  14909  cdaf  14910  imasmnd2  15450  imasgrp2  15661  efgrelexlemb  16238  efgredeu  16240  imasrng  16699  znf1o  17959  zzngim  17960  indlcim  18244  1stcfb  19024  upxp  19171  uptx  19173  cnmpt1st  19216  cnmpt2nd  19217  qtoptopon  19252  qtopcld  19261  qtopeu  19264  qtoprest  19265  imastopn  19268  qtophmeo  19365  elfm3  19498  uniiccdif  21033  dirith  22753  fargshiftfo  23475  grporn  23650  subgores  23742  vcoprnelem  23907  0vfval  23935  xppreima2  25916  1stpreima  25952  2ndpreima  25953  ffsrn  25980  cnre2csqima  26293  br1steq  27536  br2ndeq  27537  fnbigcup  27883  ovoliunnfl  28386  voliunnfl  28388  volsupnfl  28389  filnetlem4  28555
  Copyright terms: Public domain W3C validator