Definition df-f1o 6568

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6853, dff1o3 6854, dff1o4 6856, and dff1o5 6857. 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 18136. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7344, 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 8995. (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 6560	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6558	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6559	. . 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  6836  f1oeq2  6837  f1oeq3  6838  nff1o  6846  f1of1  6847  dff1o2  6853  dff1o5  6857  f1oco  6871  fo00  6884  dff1o6  7295  nvof1o  7300  fcof1od  7314  nf1oconst  7325  soisoi  7348  f1oweALT  7997  tposf1o2  8277  smoiso2  8409  f1finf1o  9305  f1finf1oOLD  9306  unfilem2  9344  fofinf1o  9372  alephiso  10138  cnref1o  13027  wwlktovf1o  14998  1arith  16965  xpsff1o  17612  isffth2  17963  ffthf1o  17966  orbsta  19331  symgsubmefmnd  19416  symgextf1o  19441  symgfixf1o  19458  odf1o1  19590  rngqiprngim  21314  znf1o  21570  cygznlem3  21588  scmatf1o  22538  m2cpmf1o  22763  pm2mpf1o  22821  reeff1o  26491  recosf1o  26577  efif1olem4  26587  mpodvdsmulf1o  27237  dvdsmulf1o  27239  negsf1o  28086  om2noseqf1o  28307  wlkswwlksf1o  29899  wwlksnextbij0  29921  clwlkclwwlkf1o  30030  clwwlkf1o  30070  eucrctshift  30262  frgrncvvdeqlem10  30327  numclwwlk1lem2f1o  30378  unopf1o  31935  2ndresdjuf1o  32660  mndlactf1o  33035  mndractf1o  33036  zringfrac  33582  lvecendof1f1o  33684  poimirlem26  37653  poimirlem27  37654  sticksstones4  42150  wessf1ornlem  45190  projf1o  45202  sumnnodd  45645  dvnprodlem1  45961  fourierdlem54  46175  fsetsnf1o  47066  cfsetsnfsetf1o  47073  fcoresf1ob  47085  f1ocof1ob  47093  imasetpreimafvbij  47393  sprsymrelf1o  47485  prproropf1o  47494  uspgrsprf1o  48065  1arymaptf1o  48565  2arymaptf1o  48576  rrx2xpref1o  48639