Definition df-f1o 6551

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6839, dff1o3 6840, dff1o4 6842, and dff1o5 6843. 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 18041. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7321, 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 8949. (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 6543	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6541	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6542	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 397	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 205	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6822  f1oeq2  6823  f1oeq3  6824  nff1o  6832  f1of1  6833  dff1o2  6839  dff1o5  6843  f1oco  6857  fo00  6870  dff1o6  7273  nvof1o  7278  fcof1od  7292  nf1oconst  7303  soisoi  7325  f1oweALT  7959  tposf1o2  8237  smoiso2  8369  f1finf1o  9271  f1finf1oOLD  9272  unfilem2  9311  fofinf1o  9327  alephiso  10093  cnref1o  12969  wwlktovf1o  14910  1arith  16860  xpsff1o  17513  isffth2  17867  ffthf1o  17870  orbsta  19177  symgsubmefmnd  19266  symgextf1o  19291  symgfixf1o  19308  odf1o1  19440  znf1o  21107  cygznlem3  21125  scmatf1o  22034  m2cpmf1o  22259  pm2mpf1o  22317  reeff1o  25959  recosf1o  26044  efif1olem4  26054  dvdsmulf1o  26698  negsf1o  27531  wlkswwlksf1o  29164  wwlksnextbij0  29186  clwlkclwwlkf1o  29295  clwwlkf1o  29335  eucrctshift  29527  frgrncvvdeqlem10  29592  numclwwlk1lem2f1o  29643  unopf1o  31200  2ndresdjuf1o  31906  poimirlem26  36562  poimirlem27  36563  sticksstones4  41013  wessf1ornlem  43930  projf1o  43944  sumnnodd  44394  dvnprodlem1  44710  fourierdlem54  44924  fsetsnf1o  45812  cfsetsnfsetf1o  45819  fcoresf1ob  45831  f1ocof1ob  45837  imasetpreimafvbij  46122  sprsymrelf1o  46214  prproropf1o  46223  isomuspgrlem2e  46548  uspgrsprf1o  46575  rngqiprngim  46837  1arymaptf1o  47378  2arymaptf1o  47389  rrx2xpref1o  47452