MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dff1o4 Unicode version

Theorem dff1o4 5615
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
dff1o4  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )

Proof of Theorem dff1o4
StepHypRef Expression
1 dff1o2 5612 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
2 3anass 940 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) ) )
3 df-rn 4822 . . . . . 6  |-  ran  F  =  dom  `' F
43eqeq1i 2387 . . . . 5  |-  ( ran 
F  =  B  <->  dom  `' F  =  B )
54anbi2i 676 . . . 4  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <-> 
( Fun  `' F  /\  dom  `' F  =  B ) )
6 df-fn 5390 . . . 4  |-  ( `' F  Fn  B  <->  ( Fun  `' F  /\  dom  `' F  =  B )
)
75, 6bitr4i 244 . . 3  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <->  `' F  Fn  B
)
87anbi2i 676 . 2  |-  ( ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) )  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
91, 2, 83bitri 263 1  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    /\ w3a 936    = wceq 1649   `'ccnv 4810   dom cdm 4811   ran crn 4812   Fun wfun 5381    Fn wfn 5382   -1-1-onto->wf1o 5386
This theorem is referenced by:  f1ocnv  5620  f1oun  5627  f1o00  5643  f1oi  5646  f1osn  5648  f1oprswap  5650  f1ompt  5823  f1ocnvd  6225  curry1  6370  curry2  6373  f1ofveu  6513  mapsnf1o2  6990  omxpenlem  7138  sbthlem9  7154  compssiso  8180  fsumrev  12482  fsumshft  12483  invf1o  13914  grpinvf1o  14781  ghmf1o  14955  srngf1o  15862  lmhmf1o  16042  hmeof1o2  17709  f1o3d  23877  fprodshft  25072  fprodrev  25073  axcontlem2  25611  cdleme51finvN  30721
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270  df-rn 4822  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394
  Copyright terms: Public domain W3C validator