Definition df-f1o 6493

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6773, dff1o3 6774, dff1o4 6776, and dff1o5 6777. 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 18016. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7265, 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 8889. (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 6485	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6483	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6484	. . 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  6756  f1oeq2  6757  f1oeq3  6758  nff1o  6766  f1of1  6767  dff1o2  6773  dff1o5  6777  f1oco  6791  fo00  6804  dff1o6  7216  nvof1o  7221  fcof1od  7235  nf1oconst  7246  soisoi  7269  f1oweALT  7914  tposf1o2  8192  smoiso2  8299  f1finf1o  9174  f1finf1oOLD  9175  unfilem2  9213  fofinf1o  9241  alephiso  10011  cnref1o  12904  wwlktovf1o  14884  1arith  16857  xpsff1o  17489  isffth2  17843  ffthf1o  17846  orbsta  19210  symgsubmefmnd  19295  symgextf1o  19320  symgfixf1o  19337  odf1o1  19469  rngqiprngim  21229  znf1o  21476  cygznlem3  21494  scmatf1o  22435  m2cpmf1o  22660  pm2mpf1o  22718  reeff1o  26373  recosf1o  26460  efif1olem4  26470  mpodvdsmulf1o  27120  dvdsmulf1o  27122  negsf1o  27983  onsiso  28192  om2noseqf1o  28218  bdayn0sf1o  28282  wlkswwlksf1o  29842  wwlksnextbij0  29864  clwlkclwwlkf1o  29973  clwwlkf1o  30013  eucrctshift  30205  frgrncvvdeqlem10  30270  numclwwlk1lem2f1o  30321  unopf1o  31878  2ndresdjuf1o  32607  mndlactf1o  32997  mndractf1o  32998  zringfrac  33504  lvecendof1f1o  33608  poimirlem26  37628  poimirlem27  37629  sticksstones4  42125  wessf1ornlem  45166  projf1o  45178  sumnnodd  45615  dvnprodlem1  45931  fourierdlem54  46145  fsetsnf1o  47042  cfsetsnfsetf1o  47049  fcoresf1ob  47061  f1ocof1ob  47069  imasetpreimafvbij  47394  sprsymrelf1o  47486  prproropf1o  47495  gpgprismgr4cycllem2  48084  uspgrsprf1o  48137  1arymaptf1o  48633  2arymaptf1o  48644  rrx2xpref1o  48707  oppff1o  49138  diag1f1o  49523  diag2f1o  49526