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

Theorem dff1o5 5650
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 5428 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
2 f1f 5606 . . . . 5  |-  ( F : A -1-1-> B  ->  F : A --> B )
32biantrurd 495 . . . 4  |-  ( F : A -1-1-> B  -> 
( ran  F  =  B 
<->  ( F : A --> B  /\  ran  F  =  B ) ) )
4 dffo2 5624 . . . 4  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
53, 4syl6rbbr 256 . . 3  |-  ( F : A -1-1-> B  -> 
( F : A -onto-> B 
<->  ran  F  =  B ) )
65pm5.32i 619 . 2  |-  ( ( F : A -1-1-> B  /\  F : A -onto-> B
)  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
71, 6bitri 241 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    = wceq 1649   ran crn 4846   -->wf 5417   -1-1->wf1 5418   -onto->wfo 5419   -1-1-onto->wf1o 5420
This theorem is referenced by:  f1orescnv  5657  domdifsn  7158  sucdom2  7270  ackbij1  8082  ackbij2  8087  fin4en1  8153  om2uzf1oi  11256  s4f1o  11828  ausisusgra  21341  pwssplit4  27067  indlcim  27186  cdleme50f1o  31040  diaf1oN  31625
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428
  Copyright terms: Public domain W3C validator