Definition df-f1o 6500

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6780, dff1o3 6781, dff1o4 6783, and dff1o5 6784. 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 18019. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7272, 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 8897. (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 6492	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6490	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6491	. . 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  6763  f1oeq2  6764  f1oeq3  6765  nff1o  6773  f1of1  6774  dff1o2  6780  dff1o5  6784  f1oco  6798  fo00  6811  dff1o6  7223  nvof1o  7228  fcof1od  7242  nf1oconst  7253  soisoi  7276  f1oweALT  7918  tposf1o2  8196  smoiso2  8303  f1finf1o  9177  unfilem2  9210  fofinf1o  9236  alephiso  10012  cnref1o  12902  wwlktovf1o  14886  1arith  16859  xpsff1o  17492  isffth2  17846  ffthf1o  17849  orbsta  19246  symgsubmefmnd  19331  symgextf1o  19356  symgfixf1o  19373  odf1o1  19505  rngqiprngim  21263  znf1o  21510  cygznlem3  21528  scmatf1o  22480  m2cpmf1o  22705  pm2mpf1o  22763  reeff1o  26417  recosf1o  26504  efif1olem4  26514  mpodvdsmulf1o  27164  dvdsmulf1o  27166  negsf1o  28054  oniso  28271  om2noseqf1o  28301  bdayn0sf1o  28370  wlkswwlksf1o  29956  wwlksnextbij0  29978  clwlkclwwlkf1o  30090  clwwlkf1o  30130  eucrctshift  30322  frgrncvvdeqlem10  30387  numclwwlk1lem2f1o  30438  unopf1o  31995  2ndresdjuf1o  32731  mndlactf1o  33114  mndractf1o  33115  zringfrac  33637  lvecendof1f1o  33792  poimirlem26  37849  poimirlem27  37850  sticksstones4  42471  wessf1ornlem  45496  projf1o  45508  sumnnodd  45943  dvnprodlem1  46257  fourierdlem54  46471  fsetsnf1o  47367  cfsetsnfsetf1o  47374  fcoresf1ob  47386  f1ocof1ob  47394  imasetpreimafvbij  47719  sprsymrelf1o  47811  prproropf1o  47820  gpgprismgr4cycllem2  48409  uspgrsprf1o  48462  1arymaptf1o  48957  2arymaptf1o  48968  rrx2xpref1o  49031  oppff1o  49461  diag1f1o  49846  diag2f1o  49849