Definition df-f1o 6530

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6814, dff1o3 6815, dff1o4 6817, and dff1o5 6818. 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 18126. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7310, 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 8939. (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 6522	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6520	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6521	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 399	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 208	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6796  f1oeq2  6797  f1oeq3  6798  nff1o  6806  f1of1  6807  dff1o2  6814  dff1o5  6818  f1oco  6832  fo00  6845  dff1o6  7261  nvof1o  7266  fcof1od  7280  nf1oconst  7291  soisoi  7314  f1oweALT  7955  tposf1o2  8234  smoiso2  8342  f1finf1o  9219  unfilem2  9252  fofinf1o  9277  alephiso  10056  cnref1o  12988  wwlktovf1o  14974  1arith  16965  xpsff1o  17599  isffth2  17953  ffthf1o  17956  orbsta  19355  symgsubmefmnd  19440  symgextf1o  19465  symgfixf1o  19482  odf1o1  19614  rngqiprngim  21376  znf1o  21605  cygznlem3  21623  scmatf1o  22594  m2cpmf1o  22819  pm2mpf1o  22877  reeff1o  26512  recosf1o  26602  efif1olem4  26612  mpodvdsmulf1o  27260  dvdsmulf1o  27262  negsf1o  28149  oniso  28366  om2noseqf1o  28396  bdayn0sf1o  28465  wlkswwlksf1o  30081  wwlksnextbij0  30103  clwlkclwwlkf1o  30215  clwwlkf1o  30255  eucrctshift  30447  frgrncvvdeqlem10  30512  numclwwlk1lem2f1o  30563  unopf1o  32121  2ndresdjuf1o  32854  mndlactf1o  33210  mndractf1o  33211  zringfrac  33752  lvecendof1f1o  33932  poimirlem26  38150  poimirlem27  38151  sticksstones4  42771  wessf1ornlem  45768  projf1o  45779  sumnnodd  46211  dvnprodlem1  46525  fourierdlem54  46739  fsetsnf1o  47653  cfsetsnfsetf1o  47660  fcoresf1ob  47672  f1ocof1ob  47680  imasetpreimafvbij  48017  sprsymrelf1o  48109  prproropf1o  48118  gpgprismgr4cycllem2  48723  uspgrsprf1o  48776  1arymaptf1o  49271  2arymaptf1o  49282  rrx2xpref1o  49345  oppff1o  49775  diag1f1o  50160  diag2f1o  50163