ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fof Unicode version

Theorem fof 5433
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof  |-  ( F : A -onto-> B  ->  F : A --> B )

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3209 . . 3  |-  ( ran 
F  =  B  ->  ran  F  C_  B )
21anim2i 342 . 2  |-  ( ( F  Fn  A  /\  ran  F  =  B )  ->  ( F  Fn  A  /\  ran  F  C_  B ) )
3 df-fo 5217 . 2  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
4 df-f 5215 . 2  |-  ( F : A --> B  <->  ( F  Fn  A  /\  ran  F  C_  B ) )
52, 3, 43imtr4i 201 1  |-  ( F : A -onto-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1353    C_ wss 3129   ran crn 4623    Fn wfn 5206   -->wf 5207   -onto->wfo 5209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142  df-f 5215  df-fo 5217
This theorem is referenced by:  fofun  5434  fofn  5435  dffo2  5437  foima  5438  resdif  5478  ffoss  5488  fconstfvm  5729  cocan2  5782  foeqcnvco  5784  focdmex  6109  algrflem  6223  algrflemg  6224  tposf2  6262  mapsn  6683  ssdomg  6771  fopwdom  6829  fidcenumlemrks  6945  fidcenumlemr  6947  ctmlemr  7100  ctm  7101  ctssdclemn0  7102  ctssdccl  7103  ctssdc  7105  enumctlemm  7106  enumct  7107  fodjuomnilemdc  7135  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  suplocexprlemdisj  7697  suplocexprlemub  7700  ennnfonelemdc  12370  ennnfonelemg  12374  ennnfonelemp1  12377  ennnfonelemhdmp1  12380  ennnfonelemkh  12383  ennnfonelemhf1o  12384  ennnfonelemex  12385  ennnfonelemhom  12386  ctinfomlemom  12398  ctinf  12401  ctiunctlemudc  12408  ctiunctlemf  12409  omctfn  12414  mhmid  12855  mhmmnd  12856  mhmfmhm  12857  ghmgrp  12858  dvrecap  13810  subctctexmid  14373  pw1nct  14375
  Copyright terms: Public domain W3C validator