MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffo2 Structured version   Visualization version   GIF version

Theorem dffo2 6587
Description: Alternate definition of an onto function. (Contributed by NM, 22-Mar-2006.)
Assertion
Ref Expression
dffo2 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))

Proof of Theorem dffo2
StepHypRef Expression
1 fof 6583 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6586 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 512 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6507 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6354 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 229 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 580 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 210 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  ran crn 5549   Fn wfn 6343  wf 6344  ontowfo 6346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-f 6352  df-fo 6354
This theorem is referenced by:  foco  6595  foconst  6596  dff1o5  6617  dffo3  6860  dffo4  6861  exfo  6863  fo1stres  7704  fo2ndres  7705  fo2ndf  7806  cantnf  9144  hsmexlem2  9837  setcepi  17336  odf1o1  18626  efgsfo  18794  pjfo  20787  xrhmeo  23477  grpofo  28203  cnpconn  32374  lnmepi  39563  dffo3f  41314  imasetpreimafvbijlemfo  43442  fargshiftfo  43479
  Copyright terms: Public domain W3C validator