Theorem dff1o5 6146

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

Step	Hyp	Ref	Expression
1		df-f1o 5895	. 2 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
2		f1f 6101	. . . . 5 |- ( F : A -1-1-> B -> F : A --> B )
3	2	biantrurd 529	. . . 4 |- ( F : A -1-1-> B -> ( ran F = B <-> ( F : A --> B /\ ran F = B ) ) )
4		dffo2 6119	. . . 4 |- ( F : A -onto-> B <-> ( F : A --> B /\ ran F = B ) )
5	3, 4	syl6rbbr 279	. . 3 |- ( F : A -1-1-> B -> ( F : A -onto-> B <-> ran F = B ) )
6	5	pm5.32i 669	. 2 |- ( ( F : A -1-1-> B /\ F : A -onto-> B ) <-> ( F : A -1-1-> B /\ ran F = B ) )
7	1, 6	bitri 264	1 |- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ ran F = B ) )

Syntax hints:   <-> wb 196   /\ wa 384   = wceq 1483   ran crn 5115   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1orescnv  6152  domdifsn  8043  sucdom2  8156  ackbij1  9060  ackbij2  9065  fin4en1  9131  om2uzf1oi  12752  s4f1o  13663  fvcosymgeq  17849  indlcim  20179  2lgslem1b  25117  ausgrusgrb  26060  usgrexmpledg  26154  cdleme50f1o  35834  diaf1oN  36419  pwssplit4  37659  meadjiunlem  40682