Definition df-f1o 5608

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5836, dff1o3 5837, dff1o4 5839, and dff1o5 5840. 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 5600	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5598	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5599	. . 3 wff F : A -onto-> B
7	5, 6	wa 370	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 187	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5822  f1oeq2  5823  f1oeq3  5824  nff1o  5829  f1of1  5830  dff1o2  5836  dff1o5  5840  f1oco  5853  fo00  5864  dff1o6  6189  nvof1o  6194  fcof1od  6207  soisoi  6234  f1oweALT  6791  tposf1o2  7007  smoiso2  7096  f1finf1o  7804  unfilem2  7842  fofinf1o  7858  alephiso  8527  cnref1o  11297  wwlktovf1o  13013  1arith  14834  xpsff1o  15425  isffth2  15772  ffthf1o  15775  orbsta  16918  symgextf1o  17015  symgfixf1o  17032  odf1o1  17159  znf1o  19053  cygznlem3  19071  scmatf1o  19488  m2cpmf1o  19712  pm2mpf1o  19770  reeff1o  23267  recosf1o  23349  efif1olem4  23359  dvdsmulf1o  23986  wlknwwlknbij  25286  wlkiswwlkbij  25293  wwlkextbij0  25305  clwwlkf1o  25371  clwlkf1oclwwlk  25424  eupatrl  25541  frgrancvvdeqlem8  25613  numclwlk1lem2f1o  25669  unopf1o  27404  ghomf1olem  30100  poimirlem26  31670  poimirlem27  31671  wessf1ornlem  37082  sumnnodd  37282  dvnprodlem1  37390  fourierdlem54  37592