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 512 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6717 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6549 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 227 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 580 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 208 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  ran crn 5677   Fn wfn 6538  wf 6539  ontowfo 6541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-f 6547  df-fo 6549
This theorem is referenced by:  focofo  6818  foconst  6820  dff1o5  6842  dffo3  7103  dffo4  7104  exfo  7106  fo1stres  8000  fo2ndres  8001  fo2ndf  8106  cantnf  9687  hsmexlem2  10421  setcepi  18037  odf1o1  19439  efgsfo  19606  pjfo  21269  xrhmeo  24461  grpofo  29747  cnpconn  34216  lnmepi  41817  dffo3f  43867  imasetpreimafvbijlemfo  46063  fargshiftfo  46100
  Copyright terms: Public domain W3C validator