Definition df-f1o 6494

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6774, dff1o3 6775, dff1o4 6777, and dff1o5 6778. 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 18047. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7268, 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 8892. (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 6486	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6484	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6485	. . 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  6757  f1oeq2  6758  f1oeq3  6759  nff1o  6767  f1of1  6768  dff1o2  6774  dff1o5  6778  f1oco  6792  fo00  6805  dff1o6  7219  nvof1o  7224  fcof1od  7238  nf1oconst  7249  soisoi  7272  f1oweALT  7914  tposf1o2  8191  smoiso2  8298  f1finf1o  9172  unfilem2  9205  fofinf1o  9231  alephiso  10009  cnref1o  12924  wwlktovf1o  14910  1arith  16887  xpsff1o  17520  isffth2  17874  ffthf1o  17877  orbsta  19277  symgsubmefmnd  19362  symgextf1o  19387  symgfixf1o  19404  odf1o1  19536  rngqiprngim  21291  znf1o  21520  cygznlem3  21538  scmatf1o  22485  m2cpmf1o  22710  pm2mpf1o  22768  reeff1o  26400  recosf1o  26487  efif1olem4  26497  mpodvdsmulf1o  27145  dvdsmulf1o  27147  negsf1o  28034  oniso  28251  om2noseqf1o  28281  bdayn0sf1o  28350  wlkswwlksf1o  29935  wwlksnextbij0  29957  clwlkclwwlkf1o  30069  clwwlkf1o  30109  eucrctshift  30301  frgrncvvdeqlem10  30366  numclwwlk1lem2f1o  30417  unopf1o  31975  2ndresdjuf1o  32711  mndlactf1o  33078  mndractf1o  33079  zringfrac  33602  lvecendof1f1o  33765  poimirlem26  37955  poimirlem27  37956  sticksstones4  42576  wessf1ornlem  45603  projf1o  45614  sumnnodd  46048  dvnprodlem1  46362  fourierdlem54  46576  fsetsnf1o  47490  cfsetsnfsetf1o  47497  fcoresf1ob  47509  f1ocof1ob  47517  imasetpreimafvbij  47854  sprsymrelf1o  47946  prproropf1o  47955  gpgprismgr4cycllem2  48560  uspgrsprf1o  48613  1arymaptf1o  49108  2arymaptf1o  49119  rrx2xpref1o  49182  oppff1o  49612  diag1f1o  49997  diag2f1o  50000