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

Theorem dff1o4 5496
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 5493 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
2 3anass 938 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) ) )
3 df-rn 4716 . . . . . 6  |-  ran  F  =  dom  `' F
43eqeq1i 2303 . . . . 5  |-  ( ran 
F  =  B  <->  dom  `' F  =  B )
54anbi2i 675 . . . 4  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <-> 
( Fun  `' F  /\  dom  `' F  =  B ) )
6 df-fn 5274 . . . 4  |-  ( `' F  Fn  B  <->  ( Fun  `' F  /\  dom  `' F  =  B )
)
75, 6bitr4i 243 . . 3  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <->  `' F  Fn  B
)
87anbi2i 675 . 2  |-  ( ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) )  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
91, 2, 83bitri 262 1  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1632   `'ccnv 4704   dom cdm 4705   ran crn 4706   Fun wfun 5265    Fn wfn 5266   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1ocnv  5501  f1oun  5508  f1o00  5524  f1oi  5527  f1osn  5529  f1oprswap  5531  f1ompt  5698  f1ocnvd  6082  curry1  6226  curry2  6229  f1ofveu  6355  mapsnf1o2  6831  omxpenlem  6979  sbthlem9  6995  compssiso  8016  fsumrev  12257  fsumshft  12258  invf1o  13687  grpinvf1o  14554  ghmf1o  14728  srngf1o  15635  lmhmf1o  15819  hmeof1o2  17470  f1o3d  23053  axcontlem2  24665  trinv  25498  cdleme51finvN  31367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-rn 4716  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278
  Copyright terms: Public domain W3C validator