Definition df-f1o 6544

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6827, dff1o3 6828, dff1o4 6830, and dff1o5 6831. 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 18184. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7328, 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 8965. (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 6536	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6534	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6535	. . 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  6809  f1oeq2  6810  f1oeq3  6811  nff1o  6819  f1of1  6820  dff1o2  6827  dff1o5  6831  f1oco  6845  fo00  6858  dff1o6  7279  nvof1o  7284  fcof1od  7298  nf1oconst  7309  soisoi  7332  f1oweALT  7972  tposf1o2  8253  smoiso2  8361  f1finf1o  9246  unfilem2  9279  fofinf1o  9302  alephiso  10104  cnref1o  13037  wwlktovf1o  15034  1arith  17023  xpsff1o  17657  isffth2  18011  ffthf1o  18014  orbsta  19441  symgsubmefmnd  19526  symgextf1o  19551  symgfixf1o  19568  odf1o1  19700  rngqiprngim  21508  znf1o  21765  cygznlem3  21783  scmatf1o  22755  m2cpmf1o  22983  pm2mpf1o  23041  reeff1o  26680  recosf1o  26770  efif1olem4  26780  mpodvdsmulf1o  27428  dvdsmulf1o  27430  negsf1o  28317  oniso  28534  om2noseqf1o  28564  bdayn0sf1o  28633  wlkswwlksf1o  30333  wwlksnextbij0  30355  clwlkclwwlkf1o  30467  clwwlkf1o  30507  eucrctshift  30709  frgrncvvdeqlem10  30774  numclwwlk1lem2f1o  30825  unopf1o  32383  2ndresdjuf1o  33110  mndlactf1o  33457  mndractf1o  33458  zringfrac  33951  lvecendof1f1o  34130  poimirlem26  38382  poimirlem27  38383  sticksstones4  43002  wessf1ornlem  46004  projf1o  46015  sumnnodd  46447  dvnprodlem1  46761  fourierdlem54  46975  fsetsnf1o  47929  cfsetsnfsetf1o  47936  fcoresf1ob  47948  f1ocof1ob  47956  imasetpreimafvbij  48293  sprsymrelf1o  48385  prproropf1o  48394  gpgprismgr4cycllem2  48999  uspgrsprf1o  49052  1arymaptf1o  49561  2arymaptf1o  49572  rrx2xpref1o  49635  oppff1o  50062  diag1f1o  50447  diag2f1o  50450