Definition df-f1o 6232

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6488, dff1o3 6489, dff1o4 6491, and dff1o5 6492. 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 17180. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6940, 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 8366. (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 6224	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6222	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6223	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 396	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 207	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6472  f1oeq2  6473  f1oeq3  6474  nff1o  6481  f1of1  6482  dff1o2  6488  dff1o5  6492  f1oco  6505  fo00  6518  dff1o6  6897  nvof1o  6902  fcof1od  6915  soisoi  6944  f1oweALT  7529  tposf1o2  7769  smoiso2  7858  f1finf1o  8591  unfilem2  8629  fofinf1o  8645  alephiso  9370  cnref1o  12234  wwlktovf1o  14157  1arith  16092  xpsff1o  16669  isffth2  17015  ffthf1o  17018  orbsta  18184  symgextf1o  18282  symgfixf1o  18299  odf1o1  18427  znf1o  20380  cygznlem3  20398  scmatf1o  20825  m2cpmf1o  21049  pm2mpf1o  21107  reeff1o  24718  recosf1o  24800  efif1olem4  24810  dvdsmulf1o  25453  wlkswwlksf1o  27344  wwlksnextbij0  27366  clwlkclwwlkf1o  27476  clwwlkf1o  27517  eucrctshift  27710  frgrncvvdeqlem10  27779  numclwwlk1lem2f1o  27830  unopf1o  29384  poimirlem26  34449  poimirlem27  34450  wessf1ornlem  40985  projf1o  40999  sumnnodd  41453  dvnprodlem1  41772  fourierdlem54  41987  sprsymrelf1o  43142  prproropf1o  43151  isomuspgrlem2e  43479  uspgrsprf1o  43506  rrx2xpref1o  44186