Theorem dff1o4 4644

Description: Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
dff1o4	|- (F:A-1-1-onto->B <-> (F Fn A /\ `'F Fn B))

Proof of Theorem dff1o4

Step	Hyp	Ref	Expression
1		dff1o2 4639	. 2 |- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))
2		3anass 862	. 2 |- ((F Fn A /\ Fun `'F /\ ran F = B) <-> (F Fn A /\ (Fun `'F /\ ran F = B)))
3		df-rn 4005	. . . . . 6 |- ran F = dom `' F
4	3	eqeq1i 1891	. . . . 5 |- (ran F = B <-> dom `' F = B)
5	4	anbi2i 538	. . . 4 |- ((Fun `'F /\ ran F = B) <-> (Fun `'F /\ dom `' F = B))
6		df-fn 4009	. . . 4 |- (`'F Fn B <-> (Fun `'F /\ dom `' F = B))
7	5, 6	bitr4i 193	. . 3 |- ((Fun `'F /\ ran F = B) <-> `'F Fn B)
8	7	anbi2i 538	. 2 |- ((F Fn A /\ (Fun `'F /\ ran F = B)) <-> (F Fn A /\ `'F Fn B))
9	1, 2, 8	3bitri 194	1 |- (F:A-1-1-onto->B <-> (F Fn A /\ `'F Fn B))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298  `'ccnv 3985  dom cdm 3986  ran crn 3987  Fun wfun 3992   Fn wfn 3993  -1-1-onto->wf1o 3997

This theorem is referenced by:  f1ocnv 4651  f1oun 4658  f1o00 4668  f1oi 4671  f1osn 4674  f1osnOLD 4675  f1ofveu 4858  curry1 5075  curry2 5078  en2d 5459  sbthlem9 5518  gapm 9462  trinv 14759  cnvtr 15016  opncldf1 15402

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605  df-rn 4005  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013

Copyright terms: Public domain