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

Theorem dff1o5 5686
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 5464 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
2 f1f 5642 . . . . 5  |-  ( F : A -1-1-> B  ->  F : A --> B )
32biantrurd 496 . . . 4  |-  ( F : A -1-1-> B  -> 
( ran  F  =  B 
<->  ( F : A --> B  /\  ran  F  =  B ) ) )
4 dffo2 5660 . . . 4  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
53, 4syl6rbbr 257 . . 3  |-  ( F : A -1-1-> B  -> 
( F : A -onto-> B 
<->  ran  F  =  B ) )
65pm5.32i 620 . 2  |-  ( ( F : A -1-1-> B  /\  F : A -onto-> B
)  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
71, 6bitri 242 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    = wceq 1653   ran crn 4882   -->wf 5453   -1-1->wf1 5454   -onto->wfo 5455   -1-1-onto->wf1o 5456
This theorem is referenced by:  f1orescnv  5693  domdifsn  7194  sucdom2  7306  ackbij1  8123  ackbij2  8128  fin4en1  8194  om2uzf1oi  11298  s4f1o  11870  ausisusgra  21385  pwssplit4  27182  indlcim  27301  cdleme50f1o  31417  diaf1oN  32002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464
  Copyright terms: Public domain W3C validator