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 6232
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6488, dff1o3 6489, dff1o4 6491, and dff1o5 6492. 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 17180. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6940, 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 8366. (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 6224 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 6222 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 6223 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 396 . 2 wff (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵)
84, 7wb 207 1 wff (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  6472  f1oeq2  6473  f1oeq3  6474  nff1o  6481  f1of1  6482  dff1o2  6488  dff1o5  6492  f1oco  6505  fo00  6518  dff1o6  6897  nvof1o  6902  fcof1od  6915  soisoi  6944  f1oweALT  7529  tposf1o2  7769  smoiso2  7858  f1finf1o  8591  unfilem2  8629  fofinf1o  8645  alephiso  9370  cnref1o  12234  wwlktovf1o  14157  1arith  16092  xpsff1o  16669  isffth2  17015  ffthf1o  17018  orbsta  18184  symgextf1o  18282  symgfixf1o  18299  odf1o1  18427  znf1o  20380  cygznlem3  20398  scmatf1o  20825  m2cpmf1o  21049  pm2mpf1o  21107  reeff1o  24718  recosf1o  24800  efif1olem4  24810  dvdsmulf1o  25453  wlkswwlksf1o  27344  wwlksnextbij0  27366  clwlkclwwlkf1o  27476  clwwlkf1o  27517  eucrctshift  27710  frgrncvvdeqlem10  27779  numclwwlk1lem2f1o  27830  unopf1o  29384  poimirlem26  34449  poimirlem27  34450  wessf1ornlem  40985  projf1o  40999  sumnnodd  41453  dvnprodlem1  41772  fourierdlem54  41987  sprsymrelf1o  43142  prproropf1o  43151  isomuspgrlem2e  43479  uspgrsprf1o  43506  rrx2xpref1o  44186
  Copyright terms: Public domain W3C validator