Definition df-f1o 6503

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6783, dff1o3 6784, dff1o4 6786, and dff1o5 6787. 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 18055. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7276, 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 8900. (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 6495	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6493	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6494	. . 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  6766  f1oeq2  6767  f1oeq3  6768  nff1o  6776  f1of1  6777  dff1o2  6783  dff1o5  6787  f1oco  6801  fo00  6814  dff1o6  7227  nvof1o  7232  fcof1od  7246  nf1oconst  7257  soisoi  7280  f1oweALT  7922  tposf1o2  8199  smoiso2  8306  f1finf1o  9180  unfilem2  9213  fofinf1o  9239  alephiso  10017  cnref1o  12932  wwlktovf1o  14918  1arith  16895  xpsff1o  17528  isffth2  17882  ffthf1o  17885  orbsta  19285  symgsubmefmnd  19370  symgextf1o  19395  symgfixf1o  19412  odf1o1  19544  rngqiprngim  21299  znf1o  21528  cygznlem3  21546  scmatf1o  22494  m2cpmf1o  22719  pm2mpf1o  22777  reeff1o  26409  recosf1o  26496  efif1olem4  26506  mpodvdsmulf1o  27154  dvdsmulf1o  27156  negsf1o  28043  oniso  28260  om2noseqf1o  28290  bdayn0sf1o  28359  wlkswwlksf1o  29944  wwlksnextbij0  29966  clwlkclwwlkf1o  30078  clwwlkf1o  30118  eucrctshift  30310  frgrncvvdeqlem10  30375  numclwwlk1lem2f1o  30426  unopf1o  31984  2ndresdjuf1o  32720  mndlactf1o  33087  mndractf1o  33088  zringfrac  33611  lvecendof1f1o  33774  poimirlem26  37964  poimirlem27  37965  sticksstones4  42585  wessf1ornlem  45612  projf1o  45623  sumnnodd  46057  dvnprodlem1  46371  fourierdlem54  46585  fsetsnf1o  47493  cfsetsnfsetf1o  47500  fcoresf1ob  47512  f1ocof1ob  47520  imasetpreimafvbij  47857  sprsymrelf1o  47949  prproropf1o  47958  gpgprismgr4cycllem2  48563  uspgrsprf1o  48616  1arymaptf1o  49111  2arymaptf1o  49122  rrx2xpref1o  49185  oppff1o  49615  diag1f1o  50000  diag2f1o  50003