Definition df-f1o 6569

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6853, dff1o3 6854, dff1o4 6856, and dff1o5 6857. 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 18144. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7343, 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 8993. (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 6561	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6559	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6560	. . 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  6836  f1oeq2  6837  f1oeq3  6838  nff1o  6846  f1of1  6847  dff1o2  6853  dff1o5  6857  f1oco  6871  fo00  6884  dff1o6  7294  nvof1o  7299  fcof1od  7313  nf1oconst  7324  soisoi  7347  f1oweALT  7995  tposf1o2  8275  smoiso2  8407  f1finf1o  9302  f1finf1oOLD  9303  unfilem2  9341  fofinf1o  9369  alephiso  10135  cnref1o  13024  wwlktovf1o  14994  1arith  16960  xpsff1o  17613  isffth2  17969  ffthf1o  17972  orbsta  19343  symgsubmefmnd  19430  symgextf1o  19455  symgfixf1o  19472  odf1o1  19604  rngqiprngim  21331  znf1o  21587  cygznlem3  21605  scmatf1o  22553  m2cpmf1o  22778  pm2mpf1o  22836  reeff1o  26505  recosf1o  26591  efif1olem4  26601  mpodvdsmulf1o  27251  dvdsmulf1o  27253  negsf1o  28100  om2noseqf1o  28321  wlkswwlksf1o  29908  wwlksnextbij0  29930  clwlkclwwlkf1o  30039  clwwlkf1o  30079  eucrctshift  30271  frgrncvvdeqlem10  30336  numclwwlk1lem2f1o  30387  unopf1o  31944  2ndresdjuf1o  32666  mndlactf1o  33017  mndractf1o  33018  zringfrac  33561  lvecendof1f1o  33660  poimirlem26  37632  poimirlem27  37633  sticksstones4  42130  wessf1ornlem  45127  projf1o  45139  sumnnodd  45585  dvnprodlem1  45901  fourierdlem54  46115  fsetsnf1o  47003  cfsetsnfsetf1o  47010  fcoresf1ob  47022  f1ocof1ob  47030  imasetpreimafvbij  47330  sprsymrelf1o  47422  prproropf1o  47431  uspgrsprf1o  47992  1arymaptf1o  48493  2arymaptf1o  48504  rrx2xpref1o  48567