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

Theorem dffo2 6462
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 6458 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6461 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 512 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6382 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6231 . . . 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 1522  ran crn 5444   Fn wfn 6220  wf 6221  ontowfo 6223
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874  df-f 6229  df-fo 6231
This theorem is referenced by:  foco  6470  foconst  6471  dff1o5  6492  dffo3  6731  dffo4  6732  exfo  6734  fo1stres  7571  fo2ndres  7572  fo2ndf  7670  cantnf  9002  hsmexlem2  9695  setcepi  17177  odf1o1  18427  efgsfo  18592  pjfo  20541  xrhmeo  23233  grpofo  27967  cnpconn  32086  lnmepi  39189  dffo3f  40997  fargshiftfo  43104
  Copyright terms: Public domain W3C validator