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

Theorem dff1o4 5817
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 5814 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
2 3anass 972 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( F  Fn  A  /\  ( Fun  `' F  /\  ran  F  =  B ) ) )
3 df-rn 5005 . . . . . 6  |-  ran  F  =  dom  `' F
43eqeq1i 2469 . . . . 5  |-  ( ran 
F  =  B  <->  dom  `' F  =  B )
54anbi2i 694 . . . 4  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <-> 
( Fun  `' F  /\  dom  `' F  =  B ) )
6 df-fn 5584 . . . 4  |-  ( `' F  Fn  B  <->  ( Fun  `' F  /\  dom  `' F  =  B )
)
75, 6bitr4i 252 . . 3  |-  ( ( Fun  `' F  /\  ran  F  =  B )  <->  `' F  Fn  B
)
87anbi2i 694 . 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 369    /\ w3a 968    = wceq 1374   `'ccnv 4993   dom cdm 4994   ran crn 4995   Fun wfun 5575    Fn wfn 5576   -1-1-onto->wf1o 5580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3478  df-ss 3485  df-rn 5005  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588
This theorem is referenced by:  f1ocnv  5821  f1oun  5828  f1o00  5841  f1oi  5844  f1osn  5846  f1oprswap  5848  f1ompt  6036  f1ofveu  6272  f1ocnvd  6501  curry1  6867  curry2  6870  mapsnf1o2  7458  omxpenlem  7610  sbthlem9  7627  compssiso  8745  mptfzshft  13544  fsumrev  13545  invf1o  15015  mhmf1o  15781  grpinvf1o  15904  ghmf1o  16086  rhmf1o  17159  srngf1o  17281  lmhmf1o  17470  hmeof1o2  19994  axcontlem2  23939  f1o3d  27132  f1od2  27207  fprodshft  28671  fprodrev  28672  cdleme51finvN  35229
  Copyright terms: Public domain W3C validator