Definition df-f1o 6534

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6818, dff1o3 6819, dff1o4 6821, and dff1o5 6822. 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 18227. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7320, 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 8961. (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 6526	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6524	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6525	. . 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  6800  f1oeq2  6801  f1oeq3  6802  nff1o  6810  f1of1  6811  dff1o2  6818  dff1o5  6822  f1oco  6836  fo00  6849  dff1o6  7271  nvof1o  7276  fcof1od  7290  nf1oconst  7301  soisoi  7324  f1oweALT  7967  tposf1o2  8247  smoiso2  8355  f1finf1o  9242  unfilem2  9276  fofinf1o  9299  alephiso  10148  cnref1o  13082  wwlktovf1o  15079  1arith  17066  xpsff1o  17700  isffth2  18054  ffthf1o  18057  orbsta  19488  symgsubmefmnd  19573  symgextf1o  19598  symgfixf1o  19615  odf1o1  19747  rngqiprngim  21561  znf1o  21818  cygznlem3  21836  scmatf1o  22808  m2cpmf1o  23036  pm2mpf1o  23094  reeff1o  26737  recosf1o  26826  efif1olem4  26836  mpodvdsmulf1o  27484  dvdsmulf1o  27486  negsf1o  28373  oniso  28590  om2noseqf1o  28620  bdayn0sf1o  28689  wlkswwlksf1o  30401  wwlksnextbij0  30423  clwlkclwwlkf1o  30535  clwwlkf1o  30575  eucrctshift  30777  frgrncvvdeqlem10  30842  numclwwlk1lem2f1o  30893  unopf1o  32451  2ndresdjuf1o  33177  mndlactf1o  33524  mndractf1o  33525  zringfrac  34019  lvecendof1f1o  34198  poimirlem26  38484  poimirlem27  38485  sticksstones4  43119  wessf1ornlem  46121  projf1o  46132  sumnnodd  46564  dvnprodlem1  46878  fourierdlem54  47092  fsetsnf1o  48046  cfsetsnfsetf1o  48053  fcoresf1ob  48065  f1ocof1ob  48073  imasetpreimafvbij  48410  sprsymrelf1o  48502  prproropf1o  48511  gpgprismgr4cycllem2  49116  uspgrsprf1o  49169  1arymaptf1o  49678  2arymaptf1o  49689  rrx2xpref1o  49752  oppff1o  50179  diag1f1o  50564  diag2f1o  50567