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

Theorem dff1o3 6624
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o3 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))

Proof of Theorem dff1o3
StepHypRef Expression
1 3anan32 1098 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6623 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6345 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 627 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 306 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1088   = wceq 1542  ccnv 5524  ran crn 5526  Fun wfun 6333   Fn wfn 6334  ontowfo 6337  1-1-ontowf1o 6338
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346
This theorem is referenced by:  f1ofo  6625  resdif  6638  f1opw  7417  f11o  7673  1stconst  7821  2ndconst  7822  curry1  7825  curry2  7828  f1o2ndf1  7844  ssdomg  8601  phplem4  8749  php3  8753  dif1enlem  8759  f1opwfi  8901  cantnfp1lem3  9216  fpwwe2lem5  10135  canthp1lem2  10153  odf1o2  18816  dprdf1o  19273  relogf1o  25310  iseupthf1o  28139  padct  30629  ballotlemfrc  32063  poimirlem1  35401  poimirlem2  35402  poimirlem3  35403  poimirlem4  35404  poimirlem6  35406  poimirlem7  35407  poimirlem9  35409  poimirlem11  35411  poimirlem12  35412  poimirlem13  35413  poimirlem14  35414  poimirlem16  35416  poimirlem17  35417  poimirlem19  35419  poimirlem20  35420  poimirlem23  35423  poimirlem24  35424  poimirlem25  35425  poimirlem29  35429  poimirlem31  35431  ntrneifv2  41236
  Copyright terms: Public domain W3C validator