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

Theorem dffo2 6809
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 6805 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6808 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 511 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6716 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6548 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 227 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 579 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 208 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1534  ran crn 5673   Fn wfn 6537  wf 6538  ontowfo 6540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961  df-f 6546  df-fo 6548
This theorem is referenced by:  focofo  6818  foconst  6820  dff1o5  6842  dffo3  7106  dffo4  7107  exfo  7109  dffo3f  7110  fo1stres  8013  fo2ndres  8014  fo2ndf  8120  cantnf  9708  hsmexlem2  10442  setcepi  18068  odf1o1  19518  efgsfo  19685  pjfo  21636  xrhmeo  24858  grpofo  30296  cnpconn  34776  lnmepi  42431  imasetpreimafvbijlemfo  46668  fargshiftfo  46705
  Copyright terms: Public domain W3C validator