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

Theorem fof 5345
Description: An onto mapping is a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
fof (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)

Proof of Theorem fof
StepHypRef Expression
1 eqimss 3151 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 339 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5129 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5127 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 200 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1331  wss 3071  ran crn 4540   Fn wfn 5118  wf 5119  ontowfo 5121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084  df-f 5127  df-fo 5129
This theorem is referenced by:  fofun  5346  fofn  5347  dffo2  5349  foima  5350  resdif  5389  ffoss  5399  fconstfvm  5638  cocan2  5689  foeqcnvco  5691  fornex  6013  algrflem  6126  algrflemg  6127  tposf2  6165  mapsn  6584  ssdomg  6672  fopwdom  6730  fidcenumlemrks  6841  fidcenumlemr  6843  ctmlemr  6993  ctm  6994  ctssdclemn0  6995  ctssdccl  6996  ctssdc  6998  enumctlemm  6999  enumct  7000  fodjuomnilemdc  7016  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  suplocexprlemdisj  7540  suplocexprlemub  7543  focdmex  10545  ennnfonelemdc  11923  ennnfonelemg  11927  ennnfonelemp1  11930  ennnfonelemhdmp1  11933  ennnfonelemkh  11936  ennnfonelemhf1o  11937  ennnfonelemex  11938  ennnfonelemhom  11939  ctinfomlemom  11951  ctinf  11954  ctiunctlemudc  11961  ctiunctlemf  11962  omctfn  11967  dvrecap  12860  subctctexmid  13301  pw1nct  13303
  Copyright terms: Public domain W3C validator