Definition df-f1o 6537

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6822, dff1o3 6823, dff1o4 6825, and dff1o5 6826. 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 18102. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7316, 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 8967. (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 6529	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6527	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6528	. . 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  6805  f1oeq2  6806  f1oeq3  6807  nff1o  6815  f1of1  6816  dff1o2  6822  dff1o5  6826  f1oco  6840  fo00  6853  dff1o6  7267  nvof1o  7272  fcof1od  7286  nf1oconst  7297  soisoi  7320  f1oweALT  7969  tposf1o2  8249  smoiso2  8381  f1finf1o  9275  f1finf1oOLD  9276  unfilem2  9314  fofinf1o  9342  alephiso  10110  cnref1o  12999  wwlktovf1o  14976  1arith  16945  xpsff1o  17579  isffth2  17929  ffthf1o  17932  orbsta  19294  symgsubmefmnd  19377  symgextf1o  19402  symgfixf1o  19419  odf1o1  19551  rngqiprngim  21263  znf1o  21510  cygznlem3  21528  scmatf1o  22468  m2cpmf1o  22693  pm2mpf1o  22751  reeff1o  26407  recosf1o  26494  efif1olem4  26504  mpodvdsmulf1o  27154  dvdsmulf1o  27156  negsf1o  28003  om2noseqf1o  28224  wlkswwlksf1o  29807  wwlksnextbij0  29829  clwlkclwwlkf1o  29938  clwwlkf1o  29978  eucrctshift  30170  frgrncvvdeqlem10  30235  numclwwlk1lem2f1o  30286  unopf1o  31843  2ndresdjuf1o  32574  mndlactf1o  32971  mndractf1o  32972  zringfrac  33515  lvecendof1f1o  33619  poimirlem26  37616  poimirlem27  37617  sticksstones4  42108  wessf1ornlem  45157  projf1o  45169  sumnnodd  45607  dvnprodlem1  45923  fourierdlem54  46137  fsetsnf1o  47031  cfsetsnfsetf1o  47038  fcoresf1ob  47050  f1ocof1ob  47058  imasetpreimafvbij  47368  sprsymrelf1o  47460  prproropf1o  47469  gpgprismgr4cycllem2  48043  uspgrsprf1o  48072  1arymaptf1o  48572  2arymaptf1o  48583  rrx2xpref1o  48646  diag1f1o  49367  diag2f1o  49370