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 5864
Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 6109, dff1o3 6110, dff1o4 6112, and dff1o5 6113. 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 16681. Therefore, two sets are called "isomorphic" if there is a bijection between them. According to isof1oidb 6539, 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 7924. (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 5856 . 2 wff 𝐹:𝐴1-1-onto𝐵
51, 2, 3wf1 5854 . . 3 wff 𝐹:𝐴1-1𝐵
61, 2, 3wfo 5855 . . 3 wff 𝐹:𝐴onto𝐵
75, 6wa 384 . 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  6094  f1oeq2  6095  f1oeq3  6096  nff1o  6102  f1of1  6103  dff1o2  6109  dff1o5  6113  f1oco  6126  fo00  6139  dff1o6  6496  nvof1o  6501  fcof1od  6514  soisoi  6543  f1oweALT  7112  tposf1o2  7338  smoiso2  7426  f1finf1o  8147  unfilem2  8185  fofinf1o  8201  alephiso  8881  cnref1o  11787  wwlktovf1o  13652  1arith  15574  xpsff1o  16168  isffth2  16516  ffthf1o  16519  orbsta  17686  symgextf1o  17783  symgfixf1o  17800  odf1o1  17927  znf1o  19840  cygznlem3  19858  scmatf1o  20278  m2cpmf1o  20502  pm2mpf1o  20560  reeff1o  24139  recosf1o  24219  efif1olem4  24229  dvdsmulf1o  24854  wlkpwwlkf1ouspgr  26668  wlknwwlksnbij  26680  wlkwwlkbij  26687  wwlksnextbij0  26699  clwwlksf1o  26819  clwlksf1oclwwlk  26870  eucrctshift  27003  frgrncvvdeqlem8  27071  numclwlk1lem2f1o  27118  unopf1o  28663  poimirlem26  33106  poimirlem27  33107  wessf1ornlem  38880  projf1o  38895  sumnnodd  39298  dvnprodlem1  39498  fourierdlem54  39714  sprsymrelf1o  41066  uspgrsprf1o  41075
  Copyright terms: Public domain W3C validator