Definition df-f1o 6495

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6775, dff1o3 6776, dff1o4 6778, and dff1o5 6779. 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 18053. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7271, 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 6487	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 6485	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 6486	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 397	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 208	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  6758  f1oeq2  6759  f1oeq3  6760  nff1o  6768  f1of1  6769  dff1o2  6775  dff1o5  6779  f1oco  6793  fo00  6806  dff1o6  7222  nvof1o  7227  fcof1od  7241  nf1oconst  7252  soisoi  7275  f1oweALT  7916  tposf1o2  8194  smoiso2  8302  f1finf1o  9177  unfilem2  9210  fofinf1o  9236  alephiso  10015  cnref1o  12930  wwlktovf1o  14916  1arith  16893  xpsff1o  17526  isffth2  17880  ffthf1o  17883  orbsta  19282  symgsubmefmnd  19367  symgextf1o  19392  symgfixf1o  19409  odf1o1  19541  rngqiprngim  21300  znf1o  21529  cygznlem3  21547  scmatf1o  22518  m2cpmf1o  22743  pm2mpf1o  22801  reeff1o  26433  recosf1o  26520  efif1olem4  26530  mpodvdsmulf1o  27178  dvdsmulf1o  27180  negsf1o  28066  oniso  28283  om2noseqf1o  28313  bdayn0sf1o  28382  wlkswwlksf1o  29967  wwlksnextbij0  29989  clwlkclwwlkf1o  30101  clwwlkf1o  30141  eucrctshift  30333  frgrncvvdeqlem10  30398  numclwwlk1lem2f1o  30449  unopf1o  32007  2ndresdjuf1o  32744  mndlactf1o  33111  mndractf1o  33112  zringfrac  33647  lvecendof1f1o  33827  poimirlem26  38026  poimirlem27  38027  sticksstones4  42647  wessf1ornlem  45644  projf1o  45655  sumnnodd  46087  dvnprodlem1  46401  fourierdlem54  46615  fsetsnf1o  47529  cfsetsnfsetf1o  47536  fcoresf1ob  47548  f1ocof1ob  47556  imasetpreimafvbij  47893  sprsymrelf1o  47985  prproropf1o  47994  gpgprismgr4cycllem2  48599  uspgrsprf1o  48652  1arymaptf1o  49147  2arymaptf1o  49158  rrx2xpref1o  49221  oppff1o  49651  diag1f1o  50036  diag2f1o  50039