Definition df-f1o 6543

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6826, dff1o3 6827, dff1o4 6829, and dff1o5 6830. 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 18154. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7322, 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 8951. (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 6535	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6533	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6534	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 400	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 209	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is used by:  f1oeq1  6808  f1oeq2  6809  f1oeq3  6810  nff1o  6818  f1of1  6819  dff1o2  6826  dff1o5  6830  f1oco  6844  fo00  6857  dff1o6  7273  nvof1o  7278  fcof1od  7292  nf1oconst  7303  soisoi  7326  f1oweALT  7967  tposf1o2  8246  smoiso2  8354  f1finf1o  9231  unfilem2  9264  fofinf1o  9287  alephiso  10089  cnref1o  13015  wwlktovf1o  15003  1arith  16993  xpsff1o  17627  isffth2  17981  ffthf1o  17984  orbsta  19389  symgsubmefmnd  19474  symgextf1o  19499  symgfixf1o  19516  odf1o1  19648  rngqiprngim  21455  znf1o  21712  cygznlem3  21730  scmatf1o  22700  m2cpmf1o  22925  pm2mpf1o  22983  reeff1o  26621  recosf1o  26711  efif1olem4  26721  mpodvdsmulf1o  27369  dvdsmulf1o  27371  negsf1o  28258  oniso  28475  om2noseqf1o  28505  bdayn0sf1o  28574  wlkswwlksf1o  30239  wwlksnextbij0  30261  clwlkclwwlkf1o  30373  clwwlkf1o  30413  eucrctshift  30605  frgrncvvdeqlem10  30670  numclwwlk1lem2f1o  30721  unopf1o  32279  2ndresdjuf1o  33006  mndlactf1o  33359  mndractf1o  33360  zringfrac  33853  lvecendof1f1o  34032  poimirlem26  38325  poimirlem27  38326  sticksstones4  42944  wessf1ornlem  45931  projf1o  45942  sumnnodd  46374  dvnprodlem1  46688  fourierdlem54  46902  fsetsnf1o  47819  cfsetsnfsetf1o  47826  fcoresf1ob  47838  f1ocof1ob  47846  imasetpreimafvbij  48183  sprsymrelf1o  48275  prproropf1o  48284  gpgprismgr4cycllem2  48889  uspgrsprf1o  48942  1arymaptf1o  49452  2arymaptf1o  49463  rrx2xpref1o  49526  oppff1o  49955  diag1f1o  50340  diag2f1o  50343