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

Theorem dffo2 6824
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 6820 . . 3 (𝐹:𝐴onto𝐵𝐹:𝐴𝐵)
2 forn 6823 . . 3 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
31, 2jca 511 . 2 (𝐹:𝐴onto𝐵 → (𝐹:𝐴𝐵 ∧ ran 𝐹 = 𝐵))
4 ffn 6736 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
5 df-fo 6567 . . . 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 1540  ran crn 5686   Fn wfn 6556  wf 6557  ontowfo 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-f 6565  df-fo 6567
This theorem is referenced by:  focofo  6833  foconst  6835  dff1o5  6857  dffo3  7122  dffo4  7123  exfo  7125  dffo3f  7126  fo1stres  8040  fo2ndres  8041  fo2ndf  8146  cantnf  9733  hsmexlem2  10467  setcepi  18133  odf1o1  19590  efgsfo  19757  pjfo  21735  xrhmeo  24977  grpofo  30518  cnpconn  35235  lnmepi  43097  imasetpreimafvbijlemfo  47392  fargshiftfo  47429
  Copyright terms: Public domain W3C validator