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

Theorem dffo2 6032
 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 6028 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6031 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 553 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 5958 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 5810 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 217 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 487 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 198 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ran crn 5039   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554  df-f 5808  df-fo 5810 This theorem is referenced by:  foco  6038  foconst  6039  dff1o5  6059  dffo3  6282  dffo4  6283  exfo  6285  fo1stres  7083  fo2ndres  7084  fo2ndf  7171  cantnf  8473  hsmexlem2  9132  setcepi  16561  odf1o1  17810  efgsfo  17975  pjfo  19878  xrhmeo  22553  fargshiftfo  26166  grpofo  26737  cnpcon  30466  lnmepi  36673  dffo3f  38359
 Copyright terms: Public domain W3C validator