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 6048
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6295, dff1o3 6296, dff1o4 6298, and dff1o5 6299. 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 16934. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6729, 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 8122. (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 6040 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 6038 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 6039 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 383 . 2 wff (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵)
84, 7wb 196 1 wff (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
Colors of variables: wff setvar class
This definition is referenced by:  f1oeq1  6280  f1oeq2  6281  f1oeq3  6282  nff1o  6288  f1of1  6289  dff1o2  6295  dff1o5  6299  f1oco  6312  fo00  6325  dff1o6  6686  nvof1o  6691  fcof1od  6704  soisoi  6733  f1oweALT  7309  tposf1o2  7539  smoiso2  7627  f1finf1o  8344  unfilem2  8382  fofinf1o  8398  alephiso  9103  cnref1o  12012  wwlktovf1o  13895  1arith  15825  xpsff1o  16422  isffth2  16769  ffthf1o  16772  orbsta  17938  symgextf1o  18035  symgfixf1o  18052  odf1o1  18179  znf1o  20094  cygznlem3  20112  scmatf1o  20532  m2cpmf1o  20756  pm2mpf1o  20814  reeff1o  24392  recosf1o  24472  efif1olem4  24482  dvdsmulf1o  25111  wlkpwwlkf1ouspgr  26980  wlknwwlksnbij  26992  wlkwwlkbij  26999  wwlksnextbij0  27011  clwlkclwwlkf1o  27126  clwwlkf1o  27172  clwlksf1oclwwlkOLD  27216  eucrctshift  27387  frgrncvvdeqlem10  27454  numclwlk1lem2f1o  27510  unopf1o  29076  poimirlem26  33740  poimirlem27  33741  wessf1ornlem  39862  projf1o  39877  sumnnodd  40357  dvnprodlem1  40656  fourierdlem54  40872  sprsymrelf1o  42250  uspgrsprf1o  42259
  Copyright terms: Public domain W3C validator