Definition df-f1o 6488

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6768, dff1o3 6769, dff1o4 6771, and dff1o5 6772. 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 17998. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7258, 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 8879. (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 6480	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6478	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6479	. . 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  6751  f1oeq2  6752  f1oeq3  6753  nff1o  6761  f1of1  6762  dff1o2  6768  dff1o5  6772  f1oco  6786  fo00  6799  dff1o6  7209  nvof1o  7214  fcof1od  7228  nf1oconst  7239  soisoi  7262  f1oweALT  7904  tposf1o2  8182  smoiso2  8289  f1finf1o  9157  unfilem2  9190  fofinf1o  9216  alephiso  9989  cnref1o  12883  wwlktovf1o  14866  1arith  16839  xpsff1o  17471  isffth2  17825  ffthf1o  17828  orbsta  19225  symgsubmefmnd  19310  symgextf1o  19335  symgfixf1o  19352  odf1o1  19484  rngqiprngim  21241  znf1o  21488  cygznlem3  21506  scmatf1o  22447  m2cpmf1o  22672  pm2mpf1o  22730  reeff1o  26384  recosf1o  26471  efif1olem4  26481  mpodvdsmulf1o  27131  dvdsmulf1o  27133  negsf1o  27996  onsiso  28205  om2noseqf1o  28231  bdayn0sf1o  28295  wlkswwlksf1o  29857  wwlksnextbij0  29879  clwlkclwwlkf1o  29991  clwwlkf1o  30031  eucrctshift  30223  frgrncvvdeqlem10  30288  numclwwlk1lem2f1o  30339  unopf1o  31896  2ndresdjuf1o  32632  mndlactf1o  33011  mndractf1o  33012  zringfrac  33519  lvecendof1f1o  33646  poimirlem26  37694  poimirlem27  37695  sticksstones4  42190  wessf1ornlem  45230  projf1o  45242  sumnnodd  45678  dvnprodlem1  45992  fourierdlem54  46206  fsetsnf1o  47093  cfsetsnfsetf1o  47100  fcoresf1ob  47112  f1ocof1ob  47120  imasetpreimafvbij  47445  sprsymrelf1o  47537  prproropf1o  47546  gpgprismgr4cycllem2  48135  uspgrsprf1o  48188  1arymaptf1o  48684  2arymaptf1o  48695  rrx2xpref1o  48758  oppff1o  49189  diag1f1o  49574  diag2f1o  49577