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 6356
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6614, dff1o3 6615, dff1o4 6617, and dff1o5 6618. 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 17341. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 7066, 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 8507. (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 6348 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 6346 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 6347 . . 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  6598  f1oeq2  6599  f1oeq3  6600  nff1o  6607  f1of1  6608  dff1o2  6614  dff1o5  6618  f1oco  6631  fo00  6644  dff1o6  7023  nvof1o  7028  fcof1od  7041  soisoi  7070  f1oweALT  7664  tposf1o2  7909  smoiso2  7997  f1finf1o  8734  unfilem2  8772  fofinf1o  8788  alephiso  9513  cnref1o  12374  wwlktovf1o  14313  1arith  16253  xpsff1o  16830  isffth2  17176  ffthf1o  17179  orbsta  18383  symgextf1o  18482  symgfixf1o  18499  odf1o1  18628  znf1o  20628  cygznlem3  20646  scmatf1o  21071  m2cpmf1o  21295  pm2mpf1o  21353  reeff1o  24964  recosf1o  25046  efif1olem4  25056  dvdsmulf1o  25699  wlkswwlksf1o  27585  wwlksnextbij0  27607  clwlkclwwlkf1o  27717  clwwlkf1o  27758  eucrctshift  27950  frgrncvvdeqlem10  28015  numclwwlk1lem2f1o  28066  unopf1o  29621  poimirlem26  34800  poimirlem27  34801  wessf1ornlem  41325  projf1o  41339  sumnnodd  41791  dvnprodlem1  42111  fourierdlem54  42326  sprsymrelf1o  43507  prproropf1o  43516  isomuspgrlem2e  43844  uspgrsprf1o  43871  symgsubmefmnd  43965  rrx2xpref1o  44603
  Copyright terms: Public domain W3C validator