Definition df-f1o 6518

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6805, dff1o3 6806, dff1o4 6808, and dff1o5 6809. 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 18053. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7299, 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 8928. (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 6510	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6508	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6509	. . 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  6788  f1oeq2  6789  f1oeq3  6790  nff1o  6798  f1of1  6799  dff1o2  6805  dff1o5  6809  f1oco  6823  fo00  6836  dff1o6  7250  nvof1o  7255  fcof1od  7269  nf1oconst  7280  soisoi  7303  f1oweALT  7951  tposf1o2  8231  smoiso2  8338  f1finf1o  9216  f1finf1oOLD  9217  unfilem2  9255  fofinf1o  9283  alephiso  10051  cnref1o  12944  wwlktovf1o  14925  1arith  16898  xpsff1o  17530  isffth2  17880  ffthf1o  17883  orbsta  19245  symgsubmefmnd  19328  symgextf1o  19353  symgfixf1o  19370  odf1o1  19502  rngqiprngim  21214  znf1o  21461  cygznlem3  21479  scmatf1o  22419  m2cpmf1o  22644  pm2mpf1o  22702  reeff1o  26357  recosf1o  26444  efif1olem4  26454  mpodvdsmulf1o  27104  dvdsmulf1o  27106  negsf1o  27960  onsiso  28169  om2noseqf1o  28195  bdayn0sf1o  28259  wlkswwlksf1o  29809  wwlksnextbij0  29831  clwlkclwwlkf1o  29940  clwwlkf1o  29980  eucrctshift  30172  frgrncvvdeqlem10  30237  numclwwlk1lem2f1o  30288  unopf1o  31845  2ndresdjuf1o  32574  mndlactf1o  32971  mndractf1o  32972  zringfrac  33525  lvecendof1f1o  33629  poimirlem26  37640  poimirlem27  37641  sticksstones4  42137  wessf1ornlem  45179  projf1o  45191  sumnnodd  45628  dvnprodlem1  45944  fourierdlem54  46158  fsetsnf1o  47052  cfsetsnfsetf1o  47059  fcoresf1ob  47071  f1ocof1ob  47079  imasetpreimafvbij  47404  sprsymrelf1o  47496  prproropf1o  47505  gpgprismgr4cycllem2  48083  uspgrsprf1o  48134  1arymaptf1o  48630  2arymaptf1o  48641  rrx2xpref1o  48704  oppff1o  49135  diag1f1o  49520  diag2f1o  49523