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

Theorem dff1o3 6110
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 1048 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6109 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 5863 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 730 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 292 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  w3a 1036   = wceq 1480  ccnv 5083  ran crn 5085  Fun wfun 5851   Fn wfn 5852  ontowfo 5855  1-1-ontowf1o 5856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864
This theorem is referenced by:  f1ofo  6111  resdif  6124  f1opw  6854  f11o  7090  1stconst  7225  2ndconst  7226  curry1  7229  curry2  7232  f1o2ndf1  7245  ssdomg  7961  phplem4  8102  php3  8106  f1opwfi  8230  cantnfp1lem3  8537  fpwwe2lem6  9417  canthp1lem2  9435  odf1o2  17928  dprdf1o  18371  relogf1o  24251  iseupthf1o  26962  padct  29381  ballotlemfrc  30411  poimirlem1  33081  poimirlem2  33082  poimirlem3  33083  poimirlem4  33084  poimirlem6  33086  poimirlem7  33087  poimirlem9  33089  poimirlem11  33091  poimirlem12  33092  poimirlem13  33093  poimirlem14  33094  poimirlem16  33096  poimirlem17  33097  poimirlem19  33099  poimirlem20  33100  poimirlem23  33103  poimirlem24  33104  poimirlem25  33105  poimirlem29  33109  poimirlem31  33111  ntrneifv2  37899
  Copyright terms: Public domain W3C validator