Definition df-f1o 6437

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6717, dff1o3 6718, dff1o4 6720, and dff1o5 6721. 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 17787. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7188, 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 8717. (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 6429	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6427	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6428	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 395	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6700  f1oeq2  6701  f1oeq3  6702  nff1o  6710  f1of1  6711  dff1o2  6717  dff1o5  6721  f1oco  6734  fo00  6747  dff1o6  7141  nvof1o  7146  fcof1od  7159  nf1oconst  7170  soisoi  7192  f1oweALT  7801  tposf1o2  8052  smoiso2  8184  f1finf1o  9007  unfilem2  9040  fofinf1o  9055  alephiso  9838  cnref1o  12707  wwlktovf1o  14655  1arith  16609  xpsff1o  17259  isffth2  17613  ffthf1o  17616  orbsta  18900  symgsubmefmnd  18987  symgextf1o  19012  symgfixf1o  19029  odf1o1  19158  znf1o  20740  cygznlem3  20758  scmatf1o  21662  m2cpmf1o  21887  pm2mpf1o  21945  reeff1o  25587  recosf1o  25672  efif1olem4  25682  dvdsmulf1o  26324  wlkswwlksf1o  28223  wwlksnextbij0  28245  clwlkclwwlkf1o  28354  clwwlkf1o  28394  eucrctshift  28586  frgrncvvdeqlem10  28651  numclwwlk1lem2f1o  28702  unopf1o  30257  2ndresdjuf1o  30966  poimirlem26  35782  poimirlem27  35783  sticksstones4  40085  wessf1ornlem  42675  projf1o  42689  sumnnodd  43125  dvnprodlem1  43441  fourierdlem54  43655  fsetsnf1o  44499  cfsetsnfsetf1o  44506  fcoresf1ob  44518  f1ocof1ob  44524  imasetpreimafvbij  44810  sprsymrelf1o  44902  prproropf1o  44911  isomuspgrlem2e  45236  uspgrsprf1o  45263  1arymaptf1o  45942  2arymaptf1o  45953  rrx2xpref1o  46016