Theorem f1o2 3684

Description: Alternate definition of one-to-one onto function.

Assertion

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

Proof of Theorem f1o2

Step	Hyp	Ref	Expression
1		df-f1 3190	. . . . . 6 |- (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))
2	1	pm3.27bi 326	. . . . 5 |- (F:A-1-1->B -> Fun `'F)
3		df-fo 3191	. . . . . 6 |- (F:A-onto->B <-> (F Fn A /\ ran F = B))
4	3	biimp 151	. . . . 5 |- (F:A-onto->B -> (F Fn A /\ ran F = B))
5	2, 4	anim12i 333	. . . 4 |- ((F:A-1-1->B /\ F:A-onto->B) -> (Fun `'F /\ (F Fn A /\ ran F = B)))
6		eqimss 2105	. . . . . . . . . 10 |- (ran F = B -> ran F (_ B)
7	6	anim2i 335	. . . . . . . . 9 |- ((F Fn A /\ ran F = B) -> (F Fn A /\ ran F (_ B))
8		df-f 3189	. . . . . . . . 9 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
9	7, 8	sylibr 200	. . . . . . . 8 |- ((F Fn A /\ ran F = B) -> F:A-->B)
10	9	anim1i 334	. . . . . . 7 |- (((F Fn A /\ ran F = B) /\ Fun `'F) -> (F:A-->B /\ Fun `'F))
11	10, 1	sylibr 200	. . . . . 6 |- (((F Fn A /\ ran F = B) /\ Fun `'F) -> F:A-1-1->B)
12	11	ancoms 436	. . . . 5 |- ((Fun `'F /\ (F Fn A /\ ran F = B)) -> F:A-1-1->B)
13	3	biimpr 152	. . . . . 6 |- ((F Fn A /\ ran F = B) -> F:A-onto->B)
14	13	adantl 388	. . . . 5 |- ((Fun `'F /\ (F Fn A /\ ran F = B)) -> F:A-onto->B)
15	12, 14	jca 288	. . . 4 |- ((Fun `'F /\ (F Fn A /\ ran F = B)) -> (F:A-1-1->B /\ F:A-onto->B))
16	5, 15	impbi 157	. . 3 |- ((F:A-1-1->B /\ F:A-onto->B) <-> (Fun `'F /\ (F Fn A /\ ran F = B)))
17		an12 484	. . 3 |- ((Fun `'F /\ (F Fn A /\ ran F = B)) <-> (F Fn A /\ (Fun `'F /\ ran F = B)))
18	16, 17	bitr 173	. 2 |- ((F:A-1-1->B /\ F:A-onto->B) <-> (F Fn A /\ (Fun `'F /\ ran F = B)))
19		df-f1o 3192	. 2 |- (F:A-1-1-onto->B <-> (F:A-1-1->B /\ F:A-onto->B))
20		3anass 778	. 2 |- ((F Fn A /\ Fun `'F /\ ran F = B) <-> (F Fn A /\ (Fun `'F /\ ran F = B)))
21	18, 19, 20	3bitr4 183	1 |- (F:A-1-1-onto->B <-> (F Fn A /\ Fun `'F /\ ran F = B))

Syntax hints:   <-> wb 146   /\ wa 223   /\ w3a 774   = wceq 954   (_ wss 2043  `'ccnv 3164  ran crn 3166  Fun wfun 3171   Fn wfn 3172  -->wf 3173  -1-1->wf1 3174  -onto->wfo 3175  -1-1-onto->wf1o 3176

This theorem is referenced by:  f1o4 3687  f1orn 3689  f1ocnv 3692  tz7.49c 3951  fiint 4540  infxpidmlem4 7506  infxpidmlem7 7509  dfrelog 8695  adj1o 9758  bra11 9979

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 776  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-f 3189  df-f1 3190  df-fo 3191  df-f1o 3192

Copyright terms: Public domain