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

Theorem dff1o5 5815
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 5585 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  F : A -onto-> B ) )
2 f1f 5771 . . . . 5  |-  ( F : A -1-1-> B  ->  F : A --> B )
32biantrurd 508 . . . 4  |-  ( F : A -1-1-> B  -> 
( ran  F  =  B 
<->  ( F : A --> B  /\  ran  F  =  B ) ) )
4 dffo2 5789 . . . 4  |-  ( F : A -onto-> B  <->  ( F : A --> B  /\  ran  F  =  B ) )
53, 4syl6rbbr 264 . . 3  |-  ( F : A -1-1-> B  -> 
( F : A -onto-> B 
<->  ran  F  =  B ) )
65pm5.32i 637 . 2  |-  ( ( F : A -1-1-> B  /\  F : A -onto-> B
)  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
71, 6bitri 249 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -1-1-> B  /\  ran  F  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1383   ran crn 4990   -->wf 5574   -1-1->wf1 5575   -onto->wfo 5576   -1-1-onto->wf1o 5577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585
This theorem is referenced by:  f1orescnv  5821  domdifsn  7602  sucdom2  7716  ackbij1  8621  ackbij2  8626  fin4en1  8692  om2uzf1oi  12043  s4f1o  12845  fvcosymgeq  16328  indlcim  18748  ausisusgra  24227  usgraexmpledg  24275  pwssplit4  31010  cdleme50f1o  36006  diaf1oN  36591
  Copyright terms: Public domain W3C validator