Definition df-f1o 6545

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6830, dff1o3 6831, dff1o4 6833, and dff1o5 6834. 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 18266. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7332, 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 8983. (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 6537	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6535	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6536	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 401	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 209	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is used by:  f1oeq1  6812  f1oeq2  6813  f1oeq3  6814  nff1o  6822  f1of1  6823  dff1o2  6830  dff1o5  6834  f1oco  6848  fo00  6861  dff1o6  7283  nvof1o  7288  fcof1od  7302  nf1oconst  7313  soisoi  7336  f1oweALT  7984  tposf1o2  8269  smoiso2  8377  f1finf1o  9264  unfilem2  9298  fofinf1o  9321  alephiso  10177  cnref1o  13113  wwlktovf1o  15112  1arith  17105  xpsff1o  17739  isffth2  18093  ffthf1o  18096  orbsta  19527  symgsubmefmnd  19612  symgextf1o  19637  symgfixf1o  19654  odf1o1  19786  rngqiprngim  21600  znf1o  21857  cygznlem3  21875  scmatf1o  22847  m2cpmf1o  23075  pm2mpf1o  23133  reeff1o  26774  recosf1o  26863  efif1olem4  26873  mpodvdsmulf1o  27521  dvdsmulf1o  27523  negsf1o  28440  oniso  28657  om2noseqf1o  28687  bdayn0sf1o  28756  wlkswwlksf1o  30468  wwlksnextbij0  30490  clwlkclwwlkf1o  30602  clwwlkf1o  30642  eucrctshift  30844  frgrncvvdeqlem10  30909  numclwwlk1lem2f1o  30960  unopf1o  32518  2ndresdjuf1o  33286  mndlactf1o  33633  mndractf1o  33634  zringfrac  34128  lvecendof1f1o  34307  poimirlem26  38607  poimirlem27  38608  sticksstones4  43242  wessf1ornlem  46242  projf1o  46253  sumnnodd  46684  dvnprodlem1  46998  fourierdlem54  47212  fsetsnf1o  48166  cfsetsnfsetf1o  48173  fcoresf1ob  48185  f1ocof1ob  48193  imasetpreimafvbij  48530  sprsymrelf1o  48622  prproropf1o  48631  gpgprismgr4cycllem2  49236  uspgrsprf1o  49289  1arymaptf1o  49798  2arymaptf1o  49809  rrx2xpref1o  49872  oppff1o  50299  diag1f1o  50684  diag2f1o  50687