Definition df-f1o 5608

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5842, dff1o3 5843, dff1o4 5845, and dff1o5 5846. 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 375	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 189	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5828  f1oeq2  5829  f1oeq3  5830  nff1o  5835  f1of1  5836  dff1o2  5842  dff1o5  5846  f1oco  5859  fo00  5871  dff1o6  6199  nvof1o  6204  fcof1od  6217  soisoi  6244  f1oweALT  6804  tposf1o2  7025  smoiso2  7114  f1finf1o  7824  unfilem2  7862  fofinf1o  7878  alephiso  8555  cnref1o  11326  wwlktovf1o  13083  1arith  14920  xpsff1o  15523  isffth2  15870  ffthf1o  15873  orbsta  17016  symgextf1o  17113  symgfixf1o  17130  odf1o1  17270  znf1o  19171  cygznlem3  19189  scmatf1o  19606  m2cpmf1o  19830  pm2mpf1o  19888  reeff1o  23451  recosf1o  23533  efif1olem4  23543  dvdsmulf1o  24172  wlknwwlknbij  25490  wlkiswwlkbij  25497  wwlkextbij0  25509  clwwlkf1o  25575  clwlkf1oclwwlk  25628  eupatrl  25745  frgrancvvdeqlem8  25817  numclwlk1lem2f1o  25873  unopf1o  27618  ghomf1olem  30361  poimirlem26  32011  poimirlem27  32012  wessf1ornlem  37497  projf1o  37512  sumnnodd  37748  dvnprodlem1  37859  fourierdlem54  38062