Definition df-f1o 6365

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6644, dff1o3 6645, dff1o4 6647, and dff1o5 6648. 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 17551. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7111, 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 8614. (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 6357	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6355	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6356	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 399	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 209	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6627  f1oeq2  6628  f1oeq3  6629  nff1o  6637  f1of1  6638  dff1o2  6644  dff1o5  6648  f1oco  6661  fo00  6674  dff1o6  7064  nvof1o  7069  fcof1od  7082  nf1oconst  7093  soisoi  7115  f1oweALT  7723  tposf1o2  7972  smoiso2  8084  f1finf1o  8880  unfilem2  8914  fofinf1o  8929  alephiso  9677  cnref1o  12546  wwlktovf1o  14491  1arith  16443  xpsff1o  17026  isffth2  17377  ffthf1o  17380  orbsta  18661  symgsubmefmnd  18744  symgextf1o  18769  symgfixf1o  18786  odf1o1  18915  znf1o  20470  cygznlem3  20488  scmatf1o  21383  m2cpmf1o  21608  pm2mpf1o  21666  reeff1o  25293  recosf1o  25378  efif1olem4  25388  dvdsmulf1o  26030  wlkswwlksf1o  27917  wwlksnextbij0  27939  clwlkclwwlkf1o  28048  clwwlkf1o  28088  eucrctshift  28280  frgrncvvdeqlem10  28345  numclwwlk1lem2f1o  28396  unopf1o  29951  2ndresdjuf1o  30660  poimirlem26  35489  poimirlem27  35490  sticksstones4  39774  wessf1ornlem  42336  projf1o  42350  sumnnodd  42789  dvnprodlem1  43105  fourierdlem54  43319  fsetsnf1o  44163  cfsetsnfsetf1o  44170  fcoresf1ob  44182  f1ocof1ob  44188  imasetpreimafvbij  44474  sprsymrelf1o  44566  prproropf1o  44575  isomuspgrlem2e  44900  uspgrsprf1o  44927  1arymaptf1o  45606  2arymaptf1o  45617  rrx2xpref1o  45680