Definition df-f1o 6104

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6354, dff1o3 6355, dff1o4 6357, and dff1o5 6358. 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 16941. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6794, 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 8197. (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 6096	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6094	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6095	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 384	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 197	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6339  f1oeq2  6340  f1oeq3  6341  nff1o  6347  f1of1  6348  dff1o2  6354  dff1o5  6358  f1oco  6371  fo00  6384  dff1o6  6751  nvof1o  6756  fcof1od  6769  soisoi  6798  f1oweALT  7378  tposf1o2  7609  smoiso2  7698  f1finf1o  8422  unfilem2  8460  fofinf1o  8476  alephiso  9200  cnref1o  12037  wwlktovf1o  13923  1arith  15844  xpsff1o  16429  isffth2  16776  ffthf1o  16779  orbsta  17943  symgextf1o  18040  symgfixf1o  18057  odf1o1  18184  znf1o  20103  cygznlem3  20121  scmatf1o  20545  m2cpmf1o  20771  pm2mpf1o  20829  reeff1o  24411  recosf1o  24492  efif1olem4  24502  dvdsmulf1o  25130  wlkswwlksf1o  27002  wlknwwlksnbijOLD  27014  wlkwwlkbijOLD  27022  wwlksnextbij0  27034  clwlkclwwlkf1o  27150  clwwlkf1o  27196  clwlksf1oclwwlkOLD  27240  eucrctshift  27412  frgrncvvdeqlem10  27479  numclwwlk1lem2f1o  27534  unopf1o  29099  poimirlem26  33743  poimirlem27  33744  wessf1ornlem  39854  projf1o  39869  sumnnodd  40336  dvnprodlem1  40635  fourierdlem54  40850  sprsymrelf1o  42310  uspgrsprf1o  42319