Definition df-f1o 6505

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6785, dff1o3 6786, dff1o4 6788, and dff1o5 6789. 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 18058. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7279, 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 8903. (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 6497	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6495	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6496	. . 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  6768  f1oeq2  6769  f1oeq3  6770  nff1o  6778  f1of1  6779  dff1o2  6785  dff1o5  6789  f1oco  6803  fo00  6816  dff1o6  7230  nvof1o  7235  fcof1od  7249  nf1oconst  7260  soisoi  7283  f1oweALT  7925  tposf1o2  8202  smoiso2  8309  f1finf1o  9183  unfilem2  9216  fofinf1o  9242  alephiso  10020  cnref1o  12935  wwlktovf1o  14921  1arith  16898  xpsff1o  17531  isffth2  17885  ffthf1o  17888  orbsta  19288  symgsubmefmnd  19373  symgextf1o  19398  symgfixf1o  19415  odf1o1  19547  rngqiprngim  21302  znf1o  21531  cygznlem3  21549  scmatf1o  22497  m2cpmf1o  22722  pm2mpf1o  22780  reeff1o  26412  recosf1o  26499  efif1olem4  26509  mpodvdsmulf1o  27157  dvdsmulf1o  27159  negsf1o  28046  oniso  28263  om2noseqf1o  28293  bdayn0sf1o  28362  wlkswwlksf1o  29947  wwlksnextbij0  29969  clwlkclwwlkf1o  30081  clwwlkf1o  30121  eucrctshift  30313  frgrncvvdeqlem10  30378  numclwwlk1lem2f1o  30429  unopf1o  31987  2ndresdjuf1o  32723  mndlactf1o  33090  mndractf1o  33091  zringfrac  33614  lvecendof1f1o  33777  poimirlem26  37967  poimirlem27  37968  sticksstones4  42588  wessf1ornlem  45615  projf1o  45626  sumnnodd  46060  dvnprodlem1  46374  fourierdlem54  46588  fsetsnf1o  47502  cfsetsnfsetf1o  47509  fcoresf1ob  47521  f1ocof1ob  47529  imasetpreimafvbij  47866  sprsymrelf1o  47958  prproropf1o  47967  gpgprismgr4cycllem2  48572  uspgrsprf1o  48625  1arymaptf1o  49120  2arymaptf1o  49131  rrx2xpref1o  49194  oppff1o  49624  diag1f1o  50009  diag2f1o  50012