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

Theorem dff1o4 5806
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 5803 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
2 3anass 975 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) ) )
3 df-rn 4999 . . . . . 6  |-  ran  F  =  dom  `' F
43eqeq1i 2461 . . . . 5  |-  ( ran 
F  =  B  <->  dom  `' F  =  B )
54anbi2i 692 . . . 4  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <-> 
( Fun  `' F  /\  dom  `' F  =  B ) )
6 df-fn 5573 . . . 4  |-  ( `' F  Fn  B  <->  ( Fun  `' F  /\  dom  `' F  =  B )
)
75, 6bitr4i 252 . . 3  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <->  `' F  Fn  B
)
87anbi2i 692 . 2  |-  ( ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) )  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
91, 2, 83bitri 271 1  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  `' F  Fn  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367    /\ w3a 971    = wceq 1398   `'ccnv 4987   dom cdm 4988   ran crn 4989   Fun wfun 5564    Fn wfn 5565   -1-1-onto->wf1o 5569
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-rn 4999  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577
This theorem is referenced by:  f1ocnv  5810  f1oun  5817  f1o00  5830  f1oi  5833  f1osn  5835  f1oprswap  5837  f1ompt  6029  f1ofveu  6265  f1ocnvd  6497  curry1  6865  curry2  6868  mapsnf1o2  7459  omxpenlem  7611  sbthlem9  7628  compssiso  8745  mptfzshft  13678  fsumrev  13679  fprodrev  13866  invf1o  15260  mhmf1o  16178  grpinvf1o  16310  ghmf1o  16498  rhmf1o  17579  srngf1o  17701  lmhmf1o  17890  hmeof1o2  20433  axcontlem2  24473  f1o3d  27693  padct  27779  f1od2  27781  mgmhmf1o  32866  rnghmf1o  32982  cdleme51finvN  36698
  Copyright terms: Public domain W3C validator