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

Theorem fof 5450
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 3221 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 342 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5234 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5232 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 201 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104   = wceq 1363  wss 3141  ran crn 4639   Fn wfn 5223  wf 5224  ontowfo 5226
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154  df-f 5232  df-fo 5234
This theorem is referenced by:  fofun  5451  fofn  5452  dffo2  5454  foima  5455  resdif  5495  ffoss  5505  fconstfvm  5747  cocan2  5802  foeqcnvco  5804  focdmex  6130  algrflem  6244  algrflemg  6245  tposf2  6283  mapsn  6704  ssdomg  6792  fopwdom  6850  fidcenumlemrks  6966  fidcenumlemr  6968  ctmlemr  7121  ctm  7122  ctssdclemn0  7123  ctssdccl  7124  ctssdc  7126  enumctlemm  7127  enumct  7128  fodjuomnilemdc  7156  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  suplocexprlemdisj  7733  suplocexprlemub  7736  ennnfonelemdc  12414  ennnfonelemg  12418  ennnfonelemp1  12421  ennnfonelemhdmp1  12424  ennnfonelemkh  12427  ennnfonelemhf1o  12428  ennnfonelemex  12429  ennnfonelemhom  12430  ctinfomlemom  12442  ctinf  12445  ctiunctlemudc  12452  ctiunctlemf  12453  omctfn  12458  imasival  12745  imasbas  12746  imasplusg  12747  imasmulr  12748  imasaddfnlemg  12753  imasaddvallemg  12754  imasaddflemg  12755  imasgrp2  13013  mhmid  13018  mhmmnd  13019  mhmfmhm  13020  ghmgrp  13021  imasring  13369  dvrecap  14530  subctctexmid  15104  pw1nct  15106
  Copyright terms: Public domain W3C validator