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

Theorem dffo2 6825
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 6821 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6824 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 511 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6737 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6569 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 228 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 580 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 209 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  ran crn 5690   Fn wfn 6558  wf 6559  ontowfo 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-f 6567  df-fo 6569
This theorem is referenced by:  focofo  6834  foconst  6836  dff1o5  6858  dffo3  7122  dffo4  7123  exfo  7125  dffo3f  7126  fo1stres  8039  fo2ndres  8040  fo2ndf  8145  cantnf  9731  hsmexlem2  10465  setcepi  18142  odf1o1  19605  efgsfo  19772  pjfo  21753  xrhmeo  24991  grpofo  30528  cnpconn  35215  lnmepi  43074  imasetpreimafvbijlemfo  47330  fargshiftfo  47367
  Copyright terms: Public domain W3C validator