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

Theorem fof 5217
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 3076 . . 3 (ran 𝐹 = 𝐵 → ran 𝐹𝐵)
21anim2i 334 . 2 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
3 df-fo 5008 . 2 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4 df-f 5006 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
52, 3, 43imtr4i 199 1 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1289  wss 2997  ran crn 4429   Fn wfn 4997  wf 4998  ontowfo 5000
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-11 1442  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-in 3003  df-ss 3010  df-f 5006  df-fo 5008
This theorem is referenced by:  fofun  5218  fofn  5219  dffo2  5221  foima  5222  resdif  5259  ffoss  5269  fconstfvm  5497  cocan2  5549  foeqcnvco  5551  fornex  5868  algrflem  5976  algrflemg  5977  tposf2  6015  mapsn  6427  ssdomg  6475  fopwdom  6532  fidcenumlemrks  6641  fidcenumlemr  6643  fodjuomnilemdc  6778  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  focdmex  10160
  Copyright terms: Public domain W3C validator