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

Theorem dff1o3 6355
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 1111 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6354 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6103 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 612 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 294 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  w3a 1100   = wceq 1637  ccnv 5310  ran crn 5312  Fun wfun 6091   Fn wfn 6092  ontowfo 6095  1-1-ontowf1o 6096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104
This theorem is referenced by:  f1ofo  6356  resdif  6369  f1opw  7115  f11o  7354  1stconst  7495  2ndconst  7496  curry1  7499  curry2  7502  f1o2ndf1  7515  ssdomg  8234  phplem4  8377  php3  8381  f1opwfi  8505  cantnfp1lem3  8820  fpwwe2lem6  9738  canthp1lem2  9756  odf1o2  18185  dprdf1o  18629  relogf1o  24523  iseupthf1o  27371  padct  29820  ballotlemfrc  30909  poimirlem1  33718  poimirlem2  33719  poimirlem3  33720  poimirlem4  33721  poimirlem6  33723  poimirlem7  33724  poimirlem9  33726  poimirlem11  33728  poimirlem12  33729  poimirlem13  33730  poimirlem14  33731  poimirlem16  33733  poimirlem17  33734  poimirlem19  33736  poimirlem20  33737  poimirlem23  33740  poimirlem24  33741  poimirlem25  33742  poimirlem29  33746  poimirlem31  33748  ntrneifv2  38872
  Copyright terms: Public domain W3C validator