MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f1o Structured version   Visualization version   GIF version

Definition df-f1o 6335
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6599, dff1o3 6600, dff1o4 6602, and dff1o5 6603. 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 17346. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7060, 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 8505. (Contributed by NM, 1-Aug-1994.)

Assertion
Ref Expression
df-f1o (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))

Detailed syntax breakdown of Definition df-f1o
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cF . . 3 class 𝐹
41, 2, 3wf1o 6327 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 6325 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 6326 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 399 . 2 wff (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵)
84, 7wb 209 1 wff (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  6583  f1oeq2  6584  f1oeq3  6585  nff1o  6592  f1of1  6593  dff1o2  6599  dff1o5  6603  f1oco  6616  fo00  6629  dff1o6  7014  nvof1o  7019  fcof1od  7032  nf1oconst  7043  soisoi  7064  f1oweALT  7659  tposf1o2  7905  smoiso2  7993  f1finf1o  8733  unfilem2  8771  fofinf1o  8787  alephiso  9513  cnref1o  12376  wwlktovf1o  14318  1arith  16256  xpsff1o  16835  isffth2  17181  ffthf1o  17184  orbsta  18438  symgsubmefmnd  18521  symgextf1o  18546  symgfixf1o  18563  odf1o1  18692  znf1o  20246  cygznlem3  20264  scmatf1o  21140  m2cpmf1o  21365  pm2mpf1o  21423  reeff1o  25045  recosf1o  25130  efif1olem4  25140  dvdsmulf1o  25782  wlkswwlksf1o  27668  wwlksnextbij0  27690  clwlkclwwlkf1o  27799  clwwlkf1o  27839  eucrctshift  28031  frgrncvvdeqlem10  28096  numclwwlk1lem2f1o  28147  unopf1o  29702  2ndresdjuf1o  30415  poimirlem26  35076  poimirlem27  35077  wessf1ornlem  41798  projf1o  41812  sumnnodd  42259  dvnprodlem1  42575  fourierdlem54  42789  imasetpreimafvbij  43910  sprsymrelf1o  44002  prproropf1o  44011  isomuspgrlem2e  44337  uspgrsprf1o  44364  1arymaptf1o  45045  2arymaptf1o  45056  rrx2xpref1o  45119
  Copyright terms: Public domain W3C validator