Definition df-f1o 6562

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6849, dff1o3 6850, dff1o4 6852, and dff1o5 6853. 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-1onto𝐵 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 18292. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7352, 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 9008. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	⊢ (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶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 6554	. 2 wff 𝐹:𝐴⟶1-1onto𝐵
5	1, 2, 3	wf1 6552	. . 3 wff 𝐹:𝐴⟶1-1𝐵
6	1, 2, 3	wfo 6553	. . 3 wff 𝐹:𝐴⟶onto𝐵
7	5, 6	wa 401	. 2 wff (𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵)
8	4, 7	wb 209	1 wff (𝐹:𝐴⟶1-1onto𝐵 ↔ (𝐹:𝐴⟶1-1𝐵 ∧ 𝐹:𝐴⟶onto𝐵))

This definition is used by:  f1oeq1  6831  f1oeq2  6832  f1oeq3  6833  nff1o  6841  f1of1  6842  dff1o2  6849  dff1o5  6853  f1oco  6867  fo00  6881  dff1o6  7303  nvof1o  7308  fcof1od  7322  nf1oconst  7333  soisoi  7356  f1oweALT  8005  tposf1o2  8294  smoiso2  8402  f1finf1o  9289  unfilem2  9323  fofinf1o  9346  alephiso  10201  cnref1o  13137  wwlktovf1o  15138  1arith  17131  xpsff1o  17765  isffth2  18119  ffthf1o  18122  orbsta  19554  symgsubmefmnd  19639  symgextf1o  19664  symgfixf1o  19681  odf1o1  19813  rngqiprngim  21627  znf1o  21884  cygznlem3  21902  scmatf1o  22874  m2cpmf1o  23102  pm2mpf1o  23160  reeff1o  26801  recosf1o  26890  efif1olem4  26900  mpodvdsmulf1o  27548  dvdsmulf1o  27550  negsf1o  28467  oniso  28684  om2noseqf1o  28714  bdayn0sf1o  28783  wlkswwlksf1o  30495  wwlksnextbij0  30517  clwlkclwwlkf1o  30629  clwwlkf1o  30669  eucrctshift  30871  frgrncvvdeqlem10  30936  numclwwlk1lem2f1o  30987  unopf1o  32545  2ndresdjuf1o  33313  mndlactf1o  33658  mndractf1o  33659  zringfrac  34153  lvecendof1f1o  34332  poimirlem26  38755  poimirlem27  38756  sticksstones4  43390  wessf1ornlem  46403  projf1o  46414  sumnnodd  46845  dvnprodlem1  47159  fourierdlem54  47373  fsetsnf1o  48327  cfsetsnfsetf1o  48334  fcoresf1ob  48346  f1ocof1ob  48354  imasetpreimafvbij  48691  sprsymrelf1o  48783  prproropf1o  48792  gpgprismgr4cycllem2  49397  uspgrsprf1o  49450  1arymaptf1o  49959  2arymaptf1o  49970  oppff1o  50468  diag1f1o  50872  diag2f1o  50878