Definition df-f1o 6580

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6867, dff1o3 6868, dff1o4 6870, and dff1o5 6871. 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 18158. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7360, 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 9013. (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 6572	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6570	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6571	. . 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  6850  f1oeq2  6851  f1oeq3  6852  nff1o  6860  f1of1  6861  dff1o2  6867  dff1o5  6871  f1oco  6885  fo00  6898  dff1o6  7311  nvof1o  7316  fcof1od  7330  nf1oconst  7341  soisoi  7364  f1oweALT  8013  tposf1o2  8293  smoiso2  8425  f1finf1o  9333  f1finf1oOLD  9334  unfilem2  9372  fofinf1o  9400  alephiso  10167  cnref1o  13050  wwlktovf1o  15008  1arith  16974  xpsff1o  17627  isffth2  17983  ffthf1o  17986  orbsta  19353  symgsubmefmnd  19440  symgextf1o  19465  symgfixf1o  19482  odf1o1  19614  rngqiprngim  21337  znf1o  21593  cygznlem3  21611  scmatf1o  22559  m2cpmf1o  22784  pm2mpf1o  22842  reeff1o  26509  recosf1o  26595  efif1olem4  26605  mpodvdsmulf1o  27255  dvdsmulf1o  27257  negsf1o  28104  om2noseqf1o  28325  wlkswwlksf1o  29912  wwlksnextbij0  29934  clwlkclwwlkf1o  30043  clwwlkf1o  30083  eucrctshift  30275  frgrncvvdeqlem10  30340  numclwwlk1lem2f1o  30391  unopf1o  31948  2ndresdjuf1o  32668  mndlactf1o  33016  mndractf1o  33017  zringfrac  33547  lvecendof1f1o  33646  poimirlem26  37606  poimirlem27  37607  sticksstones4  42106  wessf1ornlem  45092  projf1o  45104  sumnnodd  45551  dvnprodlem1  45867  fourierdlem54  46081  fsetsnf1o  46969  cfsetsnfsetf1o  46976  fcoresf1ob  46988  f1ocof1ob  46996  imasetpreimafvbij  47280  sprsymrelf1o  47372  prproropf1o  47381  uspgrsprf1o  47872  1arymaptf1o  48378  2arymaptf1o  48389  rrx2xpref1o  48452