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

Theorem dffo2 6280
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 6276 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6279 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 555 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6206 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6055 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 218 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 489 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 199 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  ran crn 5267   Fn wfn 6044  wf 6045  ontowfo 6047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729  df-f 6053  df-fo 6055
This theorem is referenced by:  foco  6286  foconst  6287  dff1o5  6307  dffo3  6537  dffo4  6538  exfo  6540  fo1stres  7359  fo2ndres  7360  fo2ndf  7452  cantnf  8763  hsmexlem2  9441  setcepi  16939  odf1o1  18187  efgsfo  18352  pjfo  20261  xrhmeo  22946  grpofo  27662  cnpconn  31519  lnmepi  38157  dffo3f  39863  fargshiftfo  41888
  Copyright terms: Public domain W3C validator