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

Theorem dffo2 6086
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 6082 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6085 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 554 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6012 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 5863 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 218 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 488 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 199 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  ran crn 5085   Fn wfn 5852  wf 5853  ontowfo 5855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-f 5861  df-fo 5863
This theorem is referenced by:  foco  6092  foconst  6093  dff1o5  6113  dffo3  6340  dffo4  6341  exfo  6343  fo1stres  7152  fo2ndres  7153  fo2ndf  7244  cantnf  8550  hsmexlem2  9209  setcepi  16678  odf1o1  17927  efgsfo  18092  pjfo  19999  xrhmeo  22685  grpofo  27241  cnpconn  30973  lnmepi  37174  dffo3f  38873  fargshiftfo  40706
  Copyright terms: Public domain W3C validator