Definition df-f1o 5585

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5811, dff1o3 5812, dff1o4 5814, and dff1o5 5815. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	|- ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 5577	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5575	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5576	. . 3 wff F : A -onto-> B
7	5, 6	wa 369	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 184	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5797  f1oeq2  5798  f1oeq3  5799  nff1o  5804  f1of1  5805  dff1o2  5811  dff1o5  5815  f1oco  5828  fo00  5839  dff1o6  6166  nvof1o  6171  fcof1od  6182  soisoi  6209  f1oweALT  6769  tposf1o2  6983  smoiso2  7042  f1finf1o  7748  unfilem2  7787  fofinf1o  7803  alephiso  8482  cnref1o  11226  wwlktovf1o  12879  1arith  14427  xpsff1o  14947  isffth2  15264  ffthf1o  15267  orbsta  16330  symgextf1o  16427  symgfixf1o  16444  odf1o1  16571  znf1o  18568  cygznlem3  18586  scmatf1o  19012  m2cpmf1o  19236  pm2mpf1o  19294  reeff1o  22820  recosf1o  22900  efif1olem4  22910  dvdsmulf1o  23448  wlknwwlknbij  24691  wlkiswwlkbij  24698  wwlkextbij0  24710  clwwlkf1o  24776  clwlkf1oclwwlk  24829  eupatrl  24946  frgrancvvdeqlem8  25018  numclwlk1lem2f1o  25074  unopf1o  26813  ghomf1olem  29012  sumnnodd  31590  dvnprodlem1  31697  fourierdlem54  31897