Theorem dff1o2 4639

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

Assertion

Ref	Expression
dff1o2	|- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))

Proof of Theorem dff1o2

Step	Hyp	Ref	Expression
1		df-f1o 4013	. 2 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
2		df-f1 4011	. . 3 |- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
3		df-fo 4012	. . 3 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4	2, 3	anbi12i 540	. 2 |- ((F:A-1-1->B /\ F:A-onto->B) <-> ((F:A-->B /\ Fun `'F) /\ (F Fn A /\ ran F = B)))
5		ancom 482	. . . 4 |- ((F:A-->B /\ (Fun `'F /\ (F Fn A /\ ran F = B))) <-> ((Fun `'F /\ (F Fn A /\ ran F = B)) /\ F:A-->B))
6		3anass 862	. . . . . 6 |- ((F Fn A /\ Fun `'F /\ ran F = B) <-> (F Fn A /\ (Fun `'F /\ ran F = B)))
7		an12 542	. . . . . 6 |- ((F Fn A /\ (Fun `'F /\ ran F = B)) <-> (Fun `'F /\ (F Fn A /\ ran F = B)))
8	6, 7	bitri 190	. . . . 5 |- ((F Fn A /\ Fun `'F /\ ran F = B) <-> (Fun `'F /\ (F Fn A /\ ran F = B)))
9	8	anbi1i 539	. . . 4 |- (((F Fn A /\ Fun `'F /\ ran F = B) /\ F:A-->B) <-> ((Fun `'F /\ (F Fn A /\ ran F = B)) /\ F:A-->B))
10	5, 9	bitr4i 193	. . 3 |- ((F:A-->B /\ (Fun `'F /\ (F Fn A /\ ran F = B))) <-> ((F Fn A /\ Fun `'F /\ ran F = B) /\ F:A-->B))
11		anass 487	. . 3 |- (((F:A-->B /\ Fun `'F) /\ (F Fn A /\ ran F = B)) <-> (F:A-->B /\ (Fun `'F /\ (F Fn A /\ ran F = B))))
12		df-f 4010	. . . . . . 7 |- (F:A-->B <-> (F Fn A /\ ran F C_ B))
13	12	biimpri 169	. . . . . 6 |- ((F Fn A /\ ran F C_ B) -> F:A-->B)
14		eqimss 2665	. . . . . 6 |- (ran F = B -> ran F C_ B)
15	13, 14	sylan2 500	. . . . 5 |- ((F Fn A /\ ran F = B) -> F:A-->B)
16	15	3adant2 895	. . . 4 |- ((F Fn A /\ Fun `'F /\ ran F = B) -> F:A-->B)
17	16	pm4.71i 699	. . 3 |- ((F Fn A /\ Fun `'F /\ ran F = B) <-> ((F Fn A /\ Fun `'F /\ ran F = B) /\ F:A-->B))
18	10, 11, 17	3bitr4i 200	. 2 |- (((F:A-->B /\ Fun `'F) /\ (F Fn A /\ ran F = B)) <-> (F Fn A /\ Fun `'F /\ ran F = B))
19	1, 4, 18	3bitri 194	1 |- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))

Syntax hints:   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   C_ wss 2593  `'ccnv 3985  ran crn 3987  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -1-1->wf1 3995  -onto->wfo 3996  -1-1-onto->wf1o 3997

This theorem is referenced by:  dff1o3 4641  dff1o4 4644  dff1o4OLD 4645  f1orn 4648  f1ocnvOLD 4652  tz7.49c 5169  fiint 5650  ordtypelem7 5690  infxpidmlem4 8824  infxpidmlem7 8827  dfrelog 10110  adj1o 11455  bra11 11679  ordtypelem7OLD 15381

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-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013

Copyright terms: Public domain