Definition df-f1o 5588

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5814, dff1o3 5815, dff1o4 5817, and dff1o5 5818. 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 5580	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5578	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5579	. . 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  5800  f1oeq2  5801  f1oeq3  5802  nff1o  5807  f1of1  5808  dff1o2  5814  dff1o5  5818  f1oco  5831  fo00  5842  dff1o6  6162  nvof1o  6167  fcof1od  6178  soisoi  6205  f1oweALT  6760  tposf1o2  6973  smoiso2  7032  f1finf1o  7738  unfilem2  7776  fofinf1o  7792  alephiso  8470  cnref1o  11206  wwlktovf1o  12849  1arith  14295  xpsff1o  14814  isffth2  15134  ffthf1o  15137  orbsta  16141  symgextf1o  16238  symgfixf1o  16256  odf1o1  16383  znf1o  18352  cygznlem3  18370  scmatf1o  18796  m2cpmf1o  19020  pm2mpf1o  19078  reeff1o  22571  recosf1o  22650  efif1olem4  22660  dvdsmulf1o  23193  wlknwwlknbij  24377  wlkiswwlkbij  24384  wwlkextbij0  24396  clwwlkf1o  24462  clwlkf1oclwwlk  24515  eupatrl  24632  frgrancvvdeqlem8  24705  numclwlk1lem2f1o  24761  unopf1o  26499  ghomf1olem  28497  sumnnodd  31129  fourierdlem54  31418