Definition df-f1o 6509

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6789, dff1o3 6790, dff1o4 6792, and dff1o5 6793. 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 18029. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7282, 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 8907. (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 6501	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6499	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6500	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 395	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 206	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6772  f1oeq2  6773  f1oeq3  6774  nff1o  6782  f1of1  6783  dff1o2  6789  dff1o5  6793  f1oco  6807  fo00  6820  dff1o6  7233  nvof1o  7238  fcof1od  7252  nf1oconst  7263  soisoi  7286  f1oweALT  7928  tposf1o2  8206  smoiso2  8313  f1finf1o  9187  unfilem2  9220  fofinf1o  9246  alephiso  10022  cnref1o  12912  wwlktovf1o  14896  1arith  16869  xpsff1o  17502  isffth2  17856  ffthf1o  17859  orbsta  19259  symgsubmefmnd  19344  symgextf1o  19369  symgfixf1o  19386  odf1o1  19518  rngqiprngim  21276  znf1o  21523  cygznlem3  21541  scmatf1o  22493  m2cpmf1o  22718  pm2mpf1o  22776  reeff1o  26430  recosf1o  26517  efif1olem4  26527  mpodvdsmulf1o  27177  dvdsmulf1o  27179  negsf1o  28067  oniso  28284  om2noseqf1o  28314  bdayn0sf1o  28383  wlkswwlksf1o  29970  wwlksnextbij0  29992  clwlkclwwlkf1o  30104  clwwlkf1o  30144  eucrctshift  30336  frgrncvvdeqlem10  30401  numclwwlk1lem2f1o  30452  unopf1o  32010  2ndresdjuf1o  32746  mndlactf1o  33129  mndractf1o  33130  zringfrac  33653  lvecendof1f1o  33817  poimirlem26  37926  poimirlem27  37927  sticksstones4  42548  wessf1ornlem  45573  projf1o  45584  sumnnodd  46019  dvnprodlem1  46333  fourierdlem54  46547  fsetsnf1o  47443  cfsetsnfsetf1o  47450  fcoresf1ob  47462  f1ocof1ob  47470  imasetpreimafvbij  47795  sprsymrelf1o  47887  prproropf1o  47896  gpgprismgr4cycllem2  48485  uspgrsprf1o  48538  1arymaptf1o  49033  2arymaptf1o  49044  rrx2xpref1o  49107  oppff1o  49537  diag1f1o  49922  diag2f1o  49925