Definition df-f1o 6444

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6730, dff1o3 6731, dff1o4 6733, and dff1o5 6734. 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 17815. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7204, 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 8752. (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 6436	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6434	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6435	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 396	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6713  f1oeq2  6714  f1oeq3  6715  nff1o  6723  f1of1  6724  dff1o2  6730  dff1o5  6734  f1oco  6748  fo00  6761  dff1o6  7156  nvof1o  7161  fcof1od  7175  nf1oconst  7186  soisoi  7208  f1oweALT  7824  tposf1o2  8077  smoiso2  8209  f1finf1o  9055  unfilem2  9088  fofinf1o  9103  alephiso  9863  cnref1o  12734  wwlktovf1o  14683  1arith  16637  xpsff1o  17287  isffth2  17641  ffthf1o  17644  orbsta  18928  symgsubmefmnd  19015  symgextf1o  19040  symgfixf1o  19057  odf1o1  19186  znf1o  20768  cygznlem3  20786  scmatf1o  21690  m2cpmf1o  21915  pm2mpf1o  21973  reeff1o  25615  recosf1o  25700  efif1olem4  25710  dvdsmulf1o  26352  wlkswwlksf1o  28253  wwlksnextbij0  28275  clwlkclwwlkf1o  28384  clwwlkf1o  28424  eucrctshift  28616  frgrncvvdeqlem10  28681  numclwwlk1lem2f1o  28732  unopf1o  30287  2ndresdjuf1o  30996  poimirlem26  35812  poimirlem27  35813  sticksstones4  40112  wessf1ornlem  42729  projf1o  42743  sumnnodd  43178  dvnprodlem1  43494  fourierdlem54  43708  fsetsnf1o  44559  cfsetsnfsetf1o  44566  fcoresf1ob  44578  f1ocof1ob  44584  imasetpreimafvbij  44869  sprsymrelf1o  44961  prproropf1o  44970  isomuspgrlem2e  45295  uspgrsprf1o  45322  1arymaptf1o  46001  2arymaptf1o  46012  rrx2xpref1o  46075