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

Theorem dffo2 6585
 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 6581 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6584 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 515 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6503 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6346 . . . 4 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
65biimpri 231 . . 3 ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
74, 6sylan 583 . 2 ((𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴onto𝐵)
83, 7impbii 212 1 (𝐹:𝐴onto𝐵 ↔ (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ran crn 5529   Fn wfn 6335  ⟶wf 6336  –onto→wfo 6338 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-f 6344  df-fo 6346 This theorem is referenced by:  foco  6593  foconst  6594  dff1o5  6616  dffo3  6865  dffo4  6866  exfo  6868  fo1stres  7725  fo2ndres  7726  fo2ndf  7828  cantnf  9202  hsmexlem2  9900  setcepi  17427  odf1o1  18777  efgsfo  18945  pjfo  20493  xrhmeo  23660  grpofo  28394  cnpconn  32720  lnmepi  40437  dffo3f  42211  imasetpreimafvbijlemfo  44339  fargshiftfo  44376
 Copyright terms: Public domain W3C validator