Definition df-f1o 6543

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6826, dff1o3 6827, dff1o4 6829, and dff1o5 6830. 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 18147. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7322, 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 8952. (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 6535	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6533	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6534	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 400	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 209	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6808  f1oeq2  6809  f1oeq3  6810  nff1o  6818  f1of1  6819  dff1o2  6826  dff1o5  6830  f1oco  6844  fo00  6857  dff1o6  7273  nvof1o  7278  fcof1od  7292  nf1oconst  7303  soisoi  7326  f1oweALT  7968  tposf1o2  8247  smoiso2  8355  f1finf1o  9232  unfilem2  9265  fofinf1o  9288  alephiso  10081  cnref1o  13008  wwlktovf1o  14995  1arith  16986  xpsff1o  17620  isffth2  17974  ffthf1o  17977  orbsta  19382  symgsubmefmnd  19467  symgextf1o  19492  symgfixf1o  19509  odf1o1  19641  rngqiprngim  21423  znf1o  21680  cygznlem3  21698  scmatf1o  22668  m2cpmf1o  22893  pm2mpf1o  22951  reeff1o  26586  recosf1o  26676  efif1olem4  26686  mpodvdsmulf1o  27334  dvdsmulf1o  27336  negsf1o  28223  oniso  28440  om2noseqf1o  28470  bdayn0sf1o  28539  wlkswwlksf1o  30194  wwlksnextbij0  30216  clwlkclwwlkf1o  30328  clwwlkf1o  30368  eucrctshift  30560  frgrncvvdeqlem10  30625  numclwwlk1lem2f1o  30676  unopf1o  32234  2ndresdjuf1o  32961  mndlactf1o  33316  mndractf1o  33317  zringfrac  33810  lvecendof1f1o  33989  poimirlem26  38241  poimirlem27  38242  sticksstones4  42862  wessf1ornlem  45851  projf1o  45862  sumnnodd  46294  dvnprodlem1  46608  fourierdlem54  46822  fsetsnf1o  47736  cfsetsnfsetf1o  47743  fcoresf1ob  47755  f1ocof1ob  47763  imasetpreimafvbij  48100  sprsymrelf1o  48192  prproropf1o  48201  gpgprismgr4cycllem2  48806  uspgrsprf1o  48859  1arymaptf1o  49369  2arymaptf1o  49380  rrx2xpref1o  49443  oppff1o  49872  diag1f1o  50257  diag2f1o  50260