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

Theorem dff1o5 5564
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o5  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )

Proof of Theorem dff1o5
StepHypRef Expression
1 df-f1o 5344 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
2 f1f 5520 . . . . 5  |-  ( F : A -1-1-> B  ->  F : A --> B )
32biantrurd 494 . . . 4  |-  ( F : A -1-1-> B  -> 
( ran  F  =  B 
<->  ( F : A --> B  /\  ran  F  =  B ) ) )
4 dffo2 5538 . . . 4  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
53, 4syl6rbbr 255 . . 3  |-  ( F : A -1-1-> B  -> 
( F : A -onto-> B 
<->  ran  F  =  B ) )
65pm5.32i 618 . 2  |-  ( ( F : A -1-1-> B  /\  F : A -onto-> B
)  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
71, 6bitri 240 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    = wceq 1642   ran crn 4772   -->wf 5333   -1-1->wf1 5334   -onto->wfo 5335   -1-1-onto->wf1o 5336
This theorem is referenced by:  f1orescnv  5571  domdifsn  7033  sucdom2  7145  ackbij1  7954  ackbij2  7959  fin4en1  8025  om2uzf1oi  11108  pwssplit4  26514  indlcim  26633  s4f1o  27504  ausisusgra  27535  cdleme50f1o  30804  diaf1oN  31389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344
  Copyright terms: Public domain W3C validator