Definition df-f1o 6497

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6777, dff1o3 6778, dff1o4 6780, and dff1o5 6781. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow).

A one-to-one onto function is also called a "bijection" or a "bijective function", 𝐹:𝐴–1-1-onto→𝐵 can be read as "𝐹 is a bijection between 𝐴 and 𝐵". Bijections are precisely the isomorphisms in the category SetCat of sets and set functions, see setciso 18013. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7268, two sets are isomorphic iff there is an isomorphism Isom regarding the identity relation. In this case, the two sets are also "equinumerous", see bren 8891. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1o 6489	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6487	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6488	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 395	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 206	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6760  f1oeq2  6761  f1oeq3  6762  nff1o  6770  f1of1  6771  dff1o2  6777  dff1o5  6781  f1oco  6795  fo00  6808  dff1o6  7219  nvof1o  7224  fcof1od  7238  nf1oconst  7249  soisoi  7272  f1oweALT  7914  tposf1o2  8192  smoiso2  8299  f1finf1o  9171  unfilem2  9204  fofinf1o  9230  alephiso  10006  cnref1o  12896  wwlktovf1o  14880  1arith  16853  xpsff1o  17486  isffth2  17840  ffthf1o  17843  orbsta  19240  symgsubmefmnd  19325  symgextf1o  19350  symgfixf1o  19367  odf1o1  19499  rngqiprngim  21257  znf1o  21504  cygznlem3  21522  scmatf1o  22474  m2cpmf1o  22699  pm2mpf1o  22757  reeff1o  26411  recosf1o  26498  efif1olem4  26508  mpodvdsmulf1o  27158  dvdsmulf1o  27160  negsf1o  28023  onsiso  28236  om2noseqf1o  28262  bdayn0sf1o  28328  wlkswwlksf1o  29901  wwlksnextbij0  29923  clwlkclwwlkf1o  30035  clwwlkf1o  30075  eucrctshift  30267  frgrncvvdeqlem10  30332  numclwwlk1lem2f1o  30383  unopf1o  31940  2ndresdjuf1o  32677  mndlactf1o  33061  mndractf1o  33062  zringfrac  33584  lvecendof1f1o  33739  poimirlem26  37786  poimirlem27  37787  sticksstones4  42342  wessf1ornlem  45371  projf1o  45383  sumnnodd  45818  dvnprodlem1  46132  fourierdlem54  46346  fsetsnf1o  47242  cfsetsnfsetf1o  47249  fcoresf1ob  47261  f1ocof1ob  47269  imasetpreimafvbij  47594  sprsymrelf1o  47686  prproropf1o  47695  gpgprismgr4cycllem2  48284  uspgrsprf1o  48337  1arymaptf1o  48832  2arymaptf1o  48843  rrx2xpref1o  48906  oppff1o  49336  diag1f1o  49721  diag2f1o  49724