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

Theorem dffo2 6810
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 6806 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6809 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 513 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6718 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6550 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 227 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 581 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 208 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  ran crn 5678   Fn wfn 6539  wf 6540  ontowfo 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-f 6548  df-fo 6550
This theorem is referenced by:  focofo  6819  foconst  6821  dff1o5  6843  dffo3  7104  dffo4  7105  exfo  7107  fo1stres  8001  fo2ndres  8002  fo2ndf  8107  cantnf  9688  hsmexlem2  10422  setcepi  18038  odf1o1  19440  efgsfo  19607  pjfo  21270  xrhmeo  24462  grpofo  29752  cnpconn  34221  lnmepi  41827  dffo3f  43877  imasetpreimafvbijlemfo  46073  fargshiftfo  46110
  Copyright terms: Public domain W3C validator