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

Theorem dff1o3 6614
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 1091 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6613 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6354 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 625 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 305 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  w3a 1081   = wceq 1530  ccnv 5547  ran crn 5549  Fun wfun 6342   Fn wfn 6343  ontowfo 6346  1-1-ontowf1o 6347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355
This theorem is referenced by:  f1ofo  6615  resdif  6628  f1opw  7393  f11o  7640  1stconst  7787  2ndconst  7788  curry1  7791  curry2  7794  f1o2ndf1  7810  ssdomg  8547  phplem4  8691  php3  8695  f1opwfi  8820  cantnfp1lem3  9135  fpwwe2lem6  10049  canthp1lem2  10067  odf1o2  18690  dprdf1o  19146  relogf1o  25142  iseupthf1o  27973  padct  30447  ballotlemfrc  31777  poimirlem1  34885  poimirlem2  34886  poimirlem3  34887  poimirlem4  34888  poimirlem6  34890  poimirlem7  34891  poimirlem9  34893  poimirlem11  34895  poimirlem12  34896  poimirlem13  34897  poimirlem14  34898  poimirlem16  34900  poimirlem17  34901  poimirlem19  34903  poimirlem20  34904  poimirlem23  34907  poimirlem24  34908  poimirlem25  34909  poimirlem29  34913  poimirlem31  34915  ntrneifv2  40420
  Copyright terms: Public domain W3C validator